Un type bien

La fête du ciné se termine. Je n'ai vu que deux films, Boulevard de la Mort et Dialogues avec mon Jardinier. J'ai beaucoup aimé les deux. Ils sont très différents, mais ont cependant un point commun: on sort des deux en réalisant comme les choses simples sont efficaces. Pour le premier je pense à la simplicité de la violence et à celle du ressort "vengeance" qui fait jubiler le public comme rarement. Pour le second il s'agit de la simplicité du retour aux sources, à la nature, au jardinage, s'opposant à la vie urbaine et une création artistique sur-intellectuallisante.

Je ne peux pour ma part me résoudre à la simplicité, et, cherchant de nouvelles lectures, je suis retombé de plus belle sur Philip K. Dick, l'embrouilleur de réalités, avec le volume un (sur deux) de l'intégrale de ses nouvelles. Et, pour changer, je code: j'enrichis le système de type de liquidsoap, et je saisis cette occasion pour écrire un quelques mots sur l'inférence de type.

Pourquoi typer ?

Lors de l'exécution d'un programme, si on ne fait rien pour s'en prémunir, certaines choses absurdes peuvent arriver. Une fonction à binaire peut ne recevoir qu'un argument, on peut se retrouver à additioner un entier et un couple de chaînes de caractères, etc. Il est difficile de prévoir exactement ces problèmes sans exécuter le programme, et cela devient impossible dès lors que le langage devient Turing puissant.

Une première approche consiste à ne rien faire, et laisser le programmeur attendre que l'erreur à l'exécution arrive. C'est litéralement nul, il faut donc donner un nom à cela ("dynamique") et balancer quelques slogans qui font bien ("de toutes façons les tests unitaires sont plus précis que le typage") pour faire bonne figure. La majorité des langages de scripts adoptent cette approche. Selon l'expression absurde à évaluer, une vraie erreur va être levée, ou l'interpréteur va adopter une solution et continuer. Par exemple, si une fonction n'est pas appelée avec tous ses arguments, l'un d'eux pourra avoir la valeur spéciale undefined. Tôt ou tard, cette valeur spéciale posera une vraie erreur (on peut imaginer que l'interpréteur refuse catégoriquement de l'additionner avec quoi que ce soit), et il sera assez difficile pour le programmeur de trouver d'où venait cet undefined, qui aura pu passer de fonction en fonction avant de poser réellement problème. Je ne vais pas en dire plus sur cette approche qui ne fait rien pour le programmeur.

Le typage peut être vu comme une sur-approximation de l'ensemble des comportements qui peuvent arriver. Parfois le typage va donc détecter un problème qui ne peut pas vraiment arriver -- si on écrit une expression absurde dans une branche morte du code. En pratique, ça reste naturel. Quelques exemples rapides: 3 aura le type int; ("trois",3) le type string*int; et la fonction fun x -> x+1 le type int ->int.

Le typage statique consiste à vérifier les types avant l'exécution du programme. Dans certains langages, le programmeur écrit les types de ses variables (C/C++, Java, ...). Cela peut devenir assez lourd. D'autres langages (OCaml, SML...) sont capables de calculer le type le plus général d'une expression, c'est ce qu'on appelle l'inférence. Quand un langage a cette propriété, c'est la panacée: on n'écrit pas les lourdes annotations de type, et on a une vérification statique du code. De plus, aucune information de type n'étant nécessaire à l'exécution, les valeurs sont représentées de façon plus compacte et manipulées de façon plus immédiate, et on obtient des programmes plus rapides.

Le bémol du typage statique inféré, c'est la complexité des messages en cas d'erreur de type. D'autre part, si le système est trop simple, cela contraindra trop le programmeur dans son utilisation du langage. Mais quand on étend le système de type, on complexifie rapidement les erreurs. Il y a là un compromis délicat.

Inférer les types

Comment deviner le type d'une expression? Il suffit de regarder de près, en commencant par les expressions élémentaires et en remontant... Prenons l'exemple de fun x -> x+1.

On commence sur 1, qui a évidemment le type int. Ensuite on rencontre x, dont le type est inconnu. Mais pour que x+1 soit valide il faut bien que x soit un entier. La fonction a donc le type int -> int. Si je la nomme f, on peut maintenant chercher le type de fun y -> f("bla"). On voit qu'on utilise f avec une chaîne comme paramètre au lieu d'un entier, c'est une erreur de type.

Polymorphisme

Une extension simple et qui fonctionne bien est le polymorphisme -- ou l'appelle généricité dans certains langages. Si j'écris fun x -> x, je ne fais aucune hypothèse sur le type de mon argument, et je pourrais utiliser cette fonction sur n'importequelle valeur. C'est possible, OCaml lui donnera par exemple le type 'a -> 'a, qui veut dire pour tout a, a -> a. Exemple moins bidon: la fonction qui retourne une liste ne fait aucune hypothèse sur le type des éléments de la liste, et aura le type 'a list -> 'a list. (Exercice pénible: faites la même chose avec Java...)

Comme inférer ces types ? Il suffit de généraliser sur les variables de type (1) qui ne sont pas instantiées et (2) qui ont été introduites dans la fonction. Quand on type fun x -> x, on vérifie le corps de la fonction sans avoir besoin d'imposer aucune contrainte au type de x, c'est encore une inconnue, que Caml note '_t. L'expression a donc le type '_t -> '_t, qu'on généralisera en 'a -> 'a.

Si par contre je type fun x -> fun y -> x, il faut faire un peu plus attention. Mauvaise solution: la fonction interne a le type '_Ty -> '_Tx, que je généralise en 'a -> 'b, l'expression complète a donc le type '_Tx -> ('a -> 'b), généralisé en 'c -> 'a -> 'b. C'est manifestement faux, car cela veut dire: je prends deux paramètres quelconque et je te renvoie un truc de n'importe quel type.

Si on applique la condition (2) sur l'exemple fun x -> fun y -> x, voila comment cela se passe. La fonction interne a le type '_Ty -> '_Tx, mais '_Tx n'a pas été introduit dans cette fonction interne. On ne généralise qu'en 'a -> '_Tx. La fonction externe a donc le type '_Tx -> 'a -> '_Tx, qu'on généralise en 'b -> 'a -> 'b. C'est correct, cela veut dire: donne moi deux paramètres, je te renvoie un truc du type du premier.

Subtilités avec les références

Encore un petit détail avant de conclure. La liste vide [] peut sans problème avoir un type polymorphe 'a list. Il n'en est pas de même pour une référence ref [], qui doit garder le type '_T list ref, sans généralisation sur '_T. On ne modifie jamais une liste: on en crée une autre qui pointe sur l'ancienne. Et il n'y a aucune problème à ce qu'une liste d'entiers finisse en pointant la même liste vide qu'une liste de chaines. Par contre on modifie une référence, c'est sa raison d'être. Si on utilise notre référence dans l'instruction r := [1] on y range une liste d'entiers cela doit forcer '_T à devenir int. Car si par la suite on utilise un élément de la liste contenue dans la référence, cela ne peut pas être n'importe quoi, ce sera un entier.

Exercice/exemple: vérifier que fun x -> ref [x] a le type 'a -> 'a list ref; que let r = ref [] in (r, fun x -> r := [x]) a le type '_T list ref * ('_T -> unit).

Liquidsoap

Pourquoi j'ai parlé de tout ça ? Ces jours ci, je rafraichis le code de l'inférence de type de liquidsoap. J'ai ces choses en tête et je crois que cela vaut le coup de les présenter. Bien sûr je n'ai pas détaillé tout ce qu'il y avait dans le système de type de liquidsoap. Mais tout ce que j'ai décrit s'y trouve. Ce qui me mène à mon second but: expliquer pourquoi toute cette technologie compliquée est nécessaire dans liquidsoap.

Pour être honnête, ce n'est nécessaire que si l'on accepte le choix des types statiques et inférés dans le langage de script de liquidsoap. Pour moi il n'y a pas photo. Ensuite, on a besoin de fonctions dans le langage pour représenter les transitions. Enfin, nous prévoyons de généraliser liquidsoap, de générateur de flux audio à générateur de flux quelconque, en ajoutant la vidéo dans un premier temps. Pour cela, il faut du polymorphisme: au lieu des objets de type source on aura des objets de type format source où le format pourra être audio, video, etc. avec des informations en fait un peu plus raffinées. Certaines de fonctions actuelles de manipulation de flux, comme le switch() qui passe d'un flux à l'autre, s'étendent naturellement à n'importe quel format. Elles auront donc un type polymorphe. Enfin, si j'ai parlé des limitations de la généralisation pour les références, c'est parce que les types source se comportent pareil.

Le truc chouette, c'est que ça me donne une super excuse pour coder ces trucs que j'adore -- et que je vais enseigner l'an prochain en TP d'un cours de M1 de l'X, au passage. Et même avant l'arrivée du support vidéo, ça rend le langage plus souple et sympa pour un nombre considérable de choses. Mais je ne vais pas me lancer là dedans, c'est assez...

Création

Je ne code plus trop ces temps-ci, après la release de liquidsoap-0.3.3. Déja, je suis pas mal occupé au labo, et ça porte ses fruits. Mais de toute façon, il faut bien qu'il y ait des périodes moins frénétiques: c'est un projet sans deadline ni client. Aucune raison de se faire du mal pour apporter une amélioration montre en main. Me voilà donc dans une période tranquille, où je me demande plutôt ce que je pourrais faire de créatif à la place.

Mes pensées vont par exemple à ce projet de projet de jeu de piste (ou ARG?) radiophonique, parti de la numbers station de Balbinus... Disséminer des pistes, principalement par le biais de quelques webradios amies, vers les éléments d'une histoire/énigme/univers caché et mystérieux. Mais quelle histoire raconter, quelle idée faire passer? Parler de l'excès de communication, de l'usure des mots? des excès de l'individualisme?

En parlant d'alliance création/technique, je suis tombé sur la ménagerie, un studio d'animation amateur sympathique, qui lie developpement open-source et création d'animations en stopmotion (jetez un oeil à la section studio, par exemple cette surprise..) Chapeau bas!

De façon moins intellectuelle, je me demande si j'accrocherais à des jeux à histoire comme un Final Fantasy ou Castlevania sur DS; et si le EEE PC sortira vraiment en Aout, au prix annoncé et en quantité suffisamment énorme :)

Bientôt deux ans..

J'anticipe un peu mais le temps passe vite, et en Septembre prochain j'entamerai ma troisième année de thèse. Pour ceux qui ne savent pas, ou pour mémoire, quelques mots sur ces derniers temps.

J'ai bouclé un article que j'aime bien, des observations mignonnes de théorie de la démonstration, dans une logique linéaire dotée de principes d'induction et coinduction. L'article a été soumis à une conférence, et rejeté. Les relecteurs n'étaient pas du domaine et ont décidé que ce n'était pas bien. Je ne vais pas trop m'étendre, le papier retente sa chance à une prochaine conférence sous peu. En plus, celle là m'enverrait en Arménie, c'est plus funky que la Suisse.

Sinon j'ai passé un week-end fatiguant mais fructueux à un workshop à Edinburgh. Les gens s'intéressaient globalement aux mêmes choses que moi, et réciproquement. J'ai pu lier quelques connaissances, et ça m'a remué quelques idées en tête. Il faisait pas beau, mais la ville est très classe dans son rôle froid et solennel. Par contre j'ai pas trouvé le moyen de me faire happer par un pub sympathique, on m'a même déconseillé d'essayer.

Pendant ce temps là Frank était au Canada et Dolebraï a peu bougé. Avant-hier on s'y est remis doucement, et il recommence à alimenter la playlist. J'écoute avec plaisir ses derniers ajouts. C'est très zen, parfait pour l'humeur du moment.

Ooomm...