OCaml n'a pas de "type families" dans ce sens; pour définir une fonction sur les types au cas par cas, on voit la fonction comme une relation entre types (donc un type paramétré ('input1, 'input2, 'output) f_or), et on définit un GADT correspondant à cette relation—dont les habitants sont les témoins dynamiques.
type open = Open
type closed = Closed
type ('a, 'b, 'c) f_or =
| Left : (open, _, open)
| Right : (_, open, open)
| Closed : (closed, closed, closed)
C'est en inspectant cette valeur-témoin que tu guides le raisonnement par cas.
Note cependant que je trouve l'idée de faire une distinction entre deux cas "open" et "closed" très artificielle. On met en valeur les limites des GADTs, qui est qu'il faut penser au moment de la définition de son type à tous les usages dans les types (les fonctions depuis ses valeurs vers les types) dont on va avoir besoin. Il me semblerait plus naturel et plus général d'avoir un typage plus général Expr Env où Env est une représentation, au niveau des types, de l'ensemble des variables libres de l'expression—une représentation assez courante est d'utiliser des emboîtements de Maybe pour "compter" le nombre de variable libres connues dans le terme: Expr (Maybe (Maybe (Maybe a)))) pour un terme à quatre variable libres connues, le type vide pour un environnement clos, et par exemple Add : Expr a -> Expr a -> Expr a et Lam : Expr (Maybe a). Ça reste difficile à utiliser et donc un choix à faire avec soin—j'aurais pour ma part tendance à préférer soit une représentation moins typée soit l'usage d'un langage mieux pensé pour les types riches comme Coq ou Idris.
[^] # Re: Un cas que gère le tagless mais pas les GADT
Posté par gasche . En réponse au journal Tagless-final ou l'art de l'interprétation modulaire.. Évalué à 3.
OCaml n'a pas de "type families" dans ce sens; pour définir une fonction sur les types au cas par cas, on voit la fonction comme une relation entre types (donc un type paramétré
('input1, 'input2, 'output) f_or), et on définit un GADT correspondant à cette relation—dont les habitants sont les témoins dynamiques.C'est en inspectant cette valeur-témoin que tu guides le raisonnement par cas.
Note cependant que je trouve l'idée de faire une distinction entre deux cas "open" et "closed" très artificielle. On met en valeur les limites des GADTs, qui est qu'il faut penser au moment de la définition de son type à tous les usages dans les types (les fonctions depuis ses valeurs vers les types) dont on va avoir besoin. Il me semblerait plus naturel et plus général d'avoir un typage plus général
Expr EnvoùEnvest une représentation, au niveau des types, de l'ensemble des variables libres de l'expression—une représentation assez courante est d'utiliser des emboîtements deMaybepour "compter" le nombre de variable libres connues dans le terme:Expr (Maybe (Maybe (Maybe a))))pour un terme à quatre variable libres connues, le type vide pour un environnement clos, et par exempleAdd : Expr a -> Expr a -> Expr aetLam : Expr (Maybe a). Ça reste difficile à utiliser et donc un choix à faire avec soin—j'aurais pour ma part tendance à préférer soit une représentation moins typée soit l'usage d'un langage mieux pensé pour les types riches comme Coq ou Idris.