Quel effet ça fait

Quelle différence entre a→b→c et a→b→c? Pour le savoir, lisez ce qui suit.

De temps en temps, je regarde un article scientifique, ou un bout de code, et je n'en suis pas satisfait. Un truc me chiffonne, ça peut se réparer, mais ya autre chose qui cloche, et au fond c'est tout bancal, ça n'en finit pas, et il vaut mieux tout remettre à plat. Ceci est arrivé récemment dans liquidsoap avec le module de décodage de fichier. Ce n'est pas intéressant de détailler, il y a juste un point dont je voulais parler. Mais avant, je trouve que c'est important de dire qu'il faut remettre les choses à plat de temps en temps.

Donc, il s'agit de décodage. Première question: qu'est ce que c'est un décodeur? J'ai mis un peu de temps à essayer plusieurs styles, pour finalement décider input -> buffer -> unit, une fonction qui prend en entrée une méthode pour lire des données, et un buffer pour écrire le résultat du décodage, et qui ne renvoie rien mais remplit le buffer un peu plus à chaque fois qu'on l'appelle.

A côté de cette notion très générique on a des notions plus spécialisées comme le type file_decoder = { fill : Frame.t -> unit ; close : unit -> unit }. C'est un enregistrement qui contient une fonction de remplissage de flux (on lui donne une frame (un morceau de flux) à remplir) et une fonction de fermeture/nettoyage où l'on libère les ressources allouées pour le décodage.

Ceci étant décidé, j'écris un bout de code générique qui emballe un décodeur pour construire un décodeur_de_fichier:

let file_decoder filename decoder =
  let input = input_from_file filename in
  let buffer = create_buffer () in
  let fill frame =
    while not_enough_data_in buffer do
      decoder input buffer
    done ;
    fill_frame_from_buffer frame buffer
  in
    { fill = fill ; close = fun () -> close input }

Vous me suivez? Maintenant, j'implémente un décodeur, pour le format MP3 en utilisant la bibliothèque mad:

let create_decoder input =
  let resampler = create_resampler () in
  let mad_stream = Mad.openstream input in
    (fun buffer ->
       let data = Mad.decode_frame_float mad_stream in
       let sample_freq,_,_ = Mad.get_output_format fd in
       let content,length =
         resampler ~audio_src_rate:(float sample_freq) data
       in
         put_audio_in_buffer buffer content length)

PAF! Vous voyez le bug? Je parie que non, en tout cas moi je l'avais raté. J'ai réussi à ne pas être d'accord avec moi même, penser a→b→c ici et a→b→c là!...

Le problème, c'est les effets. En mathématiques, une fonction prend un argument et renvoie un résultat. On ne sait pas comment ça se passe "dedans", en tout cas ça n'interagit pas sur le "dehors", et ça se passe pareil à chaque fois: même entrée, même sortie. En informatique, c'est bien plus compliqué. La fonction interagit avec le monde, elle peut afficher quelquechose à l'écran, elle peut aller chercher un résultat sur internet, dans un fichier, ou simplement dans une case mémoire qu'elle partage avec d'autres fonctions. On est ainsi habitué à avoir tout un paquet de fonctions de type a→b, puisqu'il ne s'agit pas seulement de prendre un objet de type a pour calculer un objet de type b mais aussi potentiellement de se livrer à tout un tas d'interactions avec le monde.

Mon code utilise cela, mais se prend les pieds dedans. Ce qui est joli, c'est que j'ai une "solution". Mais voyons d'abord le problème. Notre décodeur prend un canal d'entrée (input), un canal de sortie (buffer), et est supposé avoir comme effet de lire un peu de données en entrée, de les convertir et les écrire en sortie. Il ne renvoie rien d'utile (unit), tout son interet réside dans l'effet; si on l'appelle un assez grand nombre de fois, on finit par avoir assez de données dans notre buffer -- c'est ce qu'on a fait plus haut. On peut cacher un certains nombres d'informations dans le décodeur, c'était mon intention, par exemple j'y ai alloué un resampler pour convertir les données vers la bonne fréquence d'échantillonage: cet outil doit être (et est bien) crée une fois et une seule pour chaque décodeur.

Ce resampler maintient un état interne, tout comme le décodeur mad (mad_stream). Allouer ces objets est aussi un effet! Mais à quel moment a-t-il lieu? Le type ne l'indique pas: dans input->buffer->unit, après quel argument un effet peut-il avoir lieu? Dans le code de file_decoder j'utilise un décodeur comme si le seul effet était le décodage, qui a lieu une fois qu'on a renseigné l'input et l'output. Mais dans le code du décodeur MP3, pas le choix, je m'autorise un effet entre le moment où on m'a donné l'input et le moment où on me donne le décodeur. Résultat, quand on utilise file_decoder avec le create_decoder MP3, on a un son tout haché, car le décodeur et le resampleur sont reinitialisés sans arrêt, ce qui provoque la perte d'une partie des données mémorisées dans leurs buffers internes.

Ces problèmes sont très vicieux, et sont toujours un sujet de recherche active. Mais concrètement, que peut-on y faire avec les outils d'aujourd'hui? Documenter, espérer que tout le monde se comprend? Pas terrible, j'ai réussi à être en désaccord avec moi-même sur une courte période de temps. Comme d'habitude, ce serait bien si le système de type nous servait de garde fou.

En logique, la notion de focalisation (focusing) est liée à la question des effets. Une formule logique est vue comme un jeu entre deux joueurs: un qui prouve l'autre qui réfute, ou encore, l'environnement qui fournit une entrée (argument) et la machine qui renvoie une sortie (valeur de retour). Les connecteurs logiques sont attribués à l'un ou à l'autre joueur: dans (int*int)→(int*int) c'est d'abord l'environnement qui donne un argument, directement composé de deux entiers; puis la machine calcule un résultat, directement composé de deux entiers. Ici je dis directement, car on ne peut pas demander une réponse partielle à la machine, tout ceci vient d'un coup, une unique réponse à une seule question. La dynamique associée au type int→int→(int*int) est exactement la même: il n'y a pas deux questions à l'environnement, mais une seule, les deux entiers en entrée arrivent d'un coup. Là dedans, les seuls effets ne peuvent donc se situer qu'à l'interface entre les deux joueurs, dans le calcul qui se passe entre une question et une réponse.

Commençons à redescendons sur terre. Pour introduire la possibilité d'un effet, en focalisation, on peut introduire un délai. Par exemple, si on veut une paire d'entiers paresseuse (dont le contenu n'est calculé que si nécessaire), on retarde le calcul des int: (unit->int)*(unit->int). Dans l'autre sens, on peut aussi vouloir retarder le moment où un argument est passé, par exemple avec a->(unit*(b->c))... c'est ce qu'il nous faut!

On la refait avec un délai autour du décodeur, implémenté non pas comme (unit*...) mais plus agréablement avec un type variant:

type decoder = Decoder of (buffer -> unit)
type file_decoder = input -> decoder

let file_decoder filename decoder =
  let input = input_from_file filename in
  let buffer = create_buffer () in
  let Decoder f = decoder input in
  let fill frame =
    while not_enough_data_in buffer do
      f buffer
    done ;
    fill_frame_from_buffer frame buffer
  in
    { fill = fill ; close = fun () -> close input }

let create_decoder input =
  let resampler = create_resampler () in
  let mad_stream = Mad.openstream input in
    Decoder (fun buffer ->
       let data = Mad.decode_frame_float mad_stream in
       let sample_freq,_,_ = Mad.get_output_format fd in
       let content,length =
         resampler ~audio_src_rate:(float sample_freq) data
       in
         put_audio_in_buffer buffer content length)

Le code du décodeur MP3 n'a changé que d'un iota, mais cela suffit à forcer sa bonne utilisation dans file_decoder, c'est à dire à passer l'input une fois pour toute, et ne plus passer que le buffer dans les appels suivants. Vraiment? Non, à vrai dire, on peut toujours se prendre les pieds dedans, ne serait-ce que parce que c'est possible de traduire entre le vieux type de décodeur et le nouveau, en violant ainsi la logique qu'on a tenté de forcer. Mais en pratique, ce petit garde fou pousse à faire naturellement la bonne chose, ou au moins à se poser la question.

Tout est bien qui fini bien. Cette histoire pourrait aussi s'intituler "à quoi diable pourrait bien servir un type variant avec un seul constructeur?" Ou encore, "c'est fou comme de belles idées théoriques ont du sens même en dehors de leur strict cadre théorique."

Dynamisme=échec

Petite update sur le post précédent.

Après la dernière modification, je me suis rendu compte que je ne prenais pas la linéarité assez au sérieux dans la version actuelle. J'ai essayé de corriger ça, mais je n'ai pas réussi à concilier linéarité et convivialité du système de types (i.e., pas d'annotation barbare).

La morale est qu'il n'y aura probablement pas de vérification statique du boxing temporel dans liquidsoap 1.0. Ce n'est pas la mort du petit cheval, on a déja une vérification dynamique pour la fallibilité (faite à l'instantiation d'une source). J'espère donc trouver le temps d'implémenter une vérification dynamique du boxing, ce serait largement mieux que le rien actuel.

Mise en boîte

Depuis un bon moment, liquidsoap dispose d'un langage de configuration/script fonctionnel, fortement et statiquement typé, qui infère des types à la ML, le tout à l'insu de la plupart des utilisateurs. Pour liquidsoap 1.0 nous irons plus loin dans l'utilisation de concepts avancés avec (un peu) de vrai polymorphisme.

J'ai édité ce post deux ou trois dans les jours suivant sa publication. Peut-être que le blog n'était pas le format idéal.

Pourquoi?

Dans une conf liquidsoap, les fonctions sont parfois utiles pour éviter de recopier du code, ou pour spécifier une action à effectuer en réaction à certains évenements. Mais au coeur même de la génération du flux, les fonctions sont utilisées pour représenter les transitions entre pistes audio. (Détails ici.)

Cette même notion de transition pose des problèmes quant à l'écoulement du temps. Actuellement dans liquidsoap, toutes les sources de flux audio évoluent à la même vitesse, cadencées par une unique horloge. Pour calculer une transition entre deux pistes d'une même source, l'opérateur cross doit obtenir en avance le début de la piste suivante, et le combiner avec la fin de la piste en cours. Cela requiert d'accélérer cette source.

L'implémentation actuelle n'est pas une solution: Les opérateurs qui en ont besoin simulent l'action de l'horloge auprès de leur source, afin de l'accélérer. Cela marche souvent, mais il se peut que deux opérateurs lisent une même source à des vitesses différentes. Le résultat est inattendu, à éviter. Notre mission est d'éviter cela statiquement, avant même la construction des sources. Nous allons donc attacher un paramètre au type des sources, qui représentera son horloge, et spécifier dans le type des opérateurs s'ils requièrent des horloges particulières.

S'il est assez facile de bricoler le système de type pour obtenir l'effet désiré, il faut d'abord identifier les concepts "logiques" mis en jeux. J'ai honte, mais ça m'a pris du temps, car j'ai commencé par chercher dans des contrées exotiques alors que c'est assez connu, bien que pointu.

Polymorphisme

Le polymorphisme est la possibilité de former une quantification universelle sur les types. Si on a un objet de type ∀x. x->x, on peut l'instantier en une fonction de type int->int aussi bien que (bool->bool)->(bool->bool).

Dans les langages dérivés de ML, le polymorphisme est limité à une quantification externe. On peut avoir ∀x. x->x mais pas (∀x. x->x)->int->int. Le polymorphisme dans toute sa généralité, par exemple dans le système F, rend en effet l'inférence de type indécidable.

OCaml permet cependant d'aller un peu plus loin. La clé est que la création d'un type polymorphe doit être explicite dans le programme (cf. ce papier), par exemple associée à la création d'un enregistrement. Considérons la signature suivante:

(** Une source associée à l'horloge 'a *)
type 'a src

(** Une fonction qui renvoie une source qu'on peut
* associer à n'importe quelle horloge. *)
type boxed = { c : 'a. unit -> 'a src }

(** Cet opérateur prend une source en boîte,
* cela pourrait être le cross() de liquidsoap. *)
val box : boxed -> 'a src

val leaf : unit -> 'a src (* en gros, single *)
val node : 'a src list -> 'a src (* en gros, fallback *)

Voyons voir ce qu'on peut et ne peut pas faire avec ce système. On peut créer un certain nombre de sources avec leaf () initialement, elles auront le type '_a src: leur horloge est indéfinie, mais pas généralisable. On est content de ne pas voir de 'a src: cela correspondrait à une source qui peut se brancher sur toutes les horloges à la fois, non-sens. (C'est aussi pour cela qu'on n'a pas écrit boxed = { c : 'a. 'a src }, on n'aurait jamais pu construire de boîte.)

On peut passer une source de type '_a src à notre opérateur node, on obtient une autre source à la même horloge '_a. Si on passe deux sources à node, le système de type requiert que leurs horloges soient les mêmes (des inconnues '_a et '_b sont unifiées).

Maintenant, tentons de former des boîtes:

let b = box { c = leaf }
(* Gagné:
* une boîte qui nous donne une nouvelle feuille à chaque fois,
* horloge au choix. *)

let a = leaf ()
let b = box { c = fun () -> b }
(* Raté, erreur de type:
* la source a est de type '_a src,
* la fonction (fun () -> b) est de type unit -> '_a src,
* qu'on ne peut généraliser en 'a. unit -> 'a src. *)

let b =
box { c = fun () ->
let a = leaf () in
node [a;a] }
(* Gagné, on a une boîte qui nous renvoie une source composée,
* dont on peut choisir l'horloge. *)

On tient clairement le bon concept: le polymorphisme assure que l'horloge peut être choisie. En particulier on va pouvoir créer des nouvelles horloges dédiées à certaines sources (et leurs sous-sources). Reste à transférer ce petit exemple en quelquechose d'agréable à utiliser dans liquidsoap.

Liquidsoap 1.0

Actuellement dans liquidsoap, on écrit des choses comme:

music = playlist("list.txt")
backup = single("default.ogg")
source = fallback([music,backup])
transition = fun (a,b) -> ...
source = cross(transition,source)
output.icecast(source)

En collant au style de notre exemple en OCaml, nous devrions réécrire les choses ainsi:

transition = fun (a,b) -> ...
source =
cross(transition, {
music = playlist("list.txt")
backup = single("default.ogg")
fallback([music,backup])
})
output.icecast(source)

C'est trop lourd, et ma solution ne va différer que d'un epsilon du style courant:

music = playlist("list.txt")
backup = single("default.ogg")
source = fallback([music,backup])
transition = fun (a,b) -> ...
source = cross(transition,{source})
output.icecast(source)

Un point clé qui permet cette simplification est qu'on n'a besoin que d'une partie du polymorphisme: on veut la généricité, mais une seule fois. Pas besoin d'une fonction qui à chaque appel pond une source, comme dans l'exemple en Caml. Il suffit d'une seule source, tant que son horloge est générique.

Je pense qu'on ne peut pas se passer aisément du marqueur {source} qui indique qu'on généralise cette source. Il me semble acceptable de demander à l'utilisateur de marquer le coup quand il utilise cette notion complexe. (Par contre il va nous falloir choisir une syntaxe qui ne rentre pas en conflit avec l'actuel {...}, raccourci pour fun () -> ....)

Comment ça marche

J'ai une implémentation en OCaml qui me semble transposable à liquidsoap.

Comment OCaml vérifie-t-il que { c = fun () -> blah } est bien typé? Il introduit une nouvelle variable de type n pour représenter le 'a de 'a. unit -> 'a src, et vérifie qu'on peut donner le type n src à blah.

Nous allons faire la même chose, mais dans le désordre, pour permettre le genre d'écriture promis plus haut. Pour former une boîte (un type universel) sur une source, il faut que son horloge soit encore indéterminée. On vérifie cela en unifiant le type de cette source avec n src pour une nouvelle variable de type n comme OCaml faisait. Et une fois qu'on a ainsi réussit à former une boîte, on affecte cette variable à type à une valeur interdite Boom pour empêcher son utilisation ailleurs. Au lieu de créer les sources dans une zone protégée, on les crée en dehors, et on les y affecte après coup, ce qui rend alors leur horloge dénuée de sens à l'extérieur.

Un difficulté essentielle du polymorphisme vient du fait que pour inférer, on a besoin de savoir quel type universel on forme. Dans le cas de liquidsoap ma solution est très simple: on ne forme que ∀x. x src. On pourrait avoir d'autres types polymorphes, mais chacun aurait son constructeur particulier.

Ces mécanismes fonctionnent bien sur quelques exemples disponibles dans mon code:

ex0 = single ()
ex0 : '_a src # pas de généralisation, c'est comme avec ref

ex00 = let x = single () in {x}
ex00 : 'a. 'a src

ex1 = fun (x) -> cross(x)
ex1 : 'b. ('a. 'a src) -> 'b src

ex4 = fun (_) -> cross({single("blah.ogg")})
ex4 : 'a.'b. 'a -> 'b src

Un exemple plus subtil est ex2 = fun (x) -> {x}, ou la variation ex4 = fun (x) -> cross({x}) qui se rapproche de ex1. Ici une boîte est formée sur l'argument de la fonction, qui doit donc être une source. Ce genre de construction est problématique: la source doit être introduite avant son horloge. En pratique, cela se traduit par l'impossibilité de former le type de la fonction où devrait apparaitre le symbole interdit: Boom src -> 'a. 'a src.

De la webradio lambda à la λ-webradio

Un article sur quelques aspects théoriques de la conception de liquidsoap, par Samuel et moi-même, a été accepté aux Journées Francophones des Langages Applicatifs (JFLA08). Sous un titre suivant la tradition blagueuse des JFLA (e.g., Le foncteur sonne toujours deux fois) nous présentons le modèle de flux sur lequel sont construits les opérateurs de liquidsoap, puis formalisons le langage de script propre à notre outil. Ça nous change des articles purement techniques, et ça vous changera de la doc des outils de tous les jours: jetez-y donc un oeil!

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...