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.