Pour simplifier, dans un GADT par rapport au type somme classique, tu peux y mettre des fonctions en plus des type de donnés.
Non. Il n’y a pas de fonction « à l’intérieur » du type. Comme pour une somme classique, les fonctions sont indépendantes et à l’extérieur (ici c’est eval). Une somme classique s’écrirait sous la forme :
-- J’ai viré le tuple de App pour alléger
data Term = Intg Int | Add | App Term Term
eval :: Term -> Int
eval (Intg n) = n
Mais déjà là, on est bloqué aux définitions de eval Add et eval (App f x) qui retourne des fonctions de type différents. On pourrait s’en sortir en faisant retourner à eval soit un Int, soit une fonction (de deux types possibles), mais il faudrait alors tester qu’on a bien une fonction pour f dans eval (App f x) par exemple, et ça serait un test à l’exécution (avec du pattern matching développé ailleurs dans ce journal) et non pas à la compilation. Or c’est non seulement lent (exécution), inutile (le développeur ne veut jamais passer autre chose que des fonctions à App), verbeux et mal extensible (il faut rajouter tout le code de pattern matching), et sources de bugs (le compilateur aurait vu tout de suite à la compilation qu’il y avait un problème).
On peut vouloir dire au compilateur que chaque terme sera évalué à un type particulier, en lui associant un phantom type, sous la forme data Term a = ... | App (Term a) (Term a). Ainsi à chaque terme est associé un type à la compilation (il est viré à l’exécution). Mais ça ne résout pas nos problèmes, en ayant eval :: Term a -> a, il n’y a pas assez de contraintes sur a pour que le compilateur empêche un utilisateur d’écrire eval (Intg 123) :: String par exemple (en gros de convertir n’importe comment). La solution c’est d’utiliser les GADTs, qui vont apporter la flexibilité d’écriture nécessaire (le compilateur déduit que eval (Intg n) retourne un Int, et que eval Add retourne un Int->Int->Int), et la sécurité du système de types, en résumant (mal) le manuel d’OCaml :
Les GADTs sont un type somme avec des contraintes de type vérifiées à la compilation.
PS : On peut simplifier le code que j’ai donné au dessus, genre avec eval Add = (+).
[^] # Re: langage fonctionnel
Posté par neil . En réponse au journal Ada, langage et ressources. Évalué à 3.
Non. Il n’y a pas de fonction « à l’intérieur » du type. Comme pour une somme classique, les fonctions sont indépendantes et à l’extérieur (ici c’est
eval). Une somme classique s’écrirait sous la forme :Mais déjà là, on est bloqué aux définitions de
eval Addeteval (App f x)qui retourne des fonctions de type différents. On pourrait s’en sortir en faisant retourner àevalsoit unInt, soit une fonction (de deux types possibles), mais il faudrait alors tester qu’on a bien une fonction pourfdanseval (App f x)par exemple, et ça serait un test à l’exécution (avec du pattern matching développé ailleurs dans ce journal) et non pas à la compilation. Or c’est non seulement lent (exécution), inutile (le développeur ne veut jamais passer autre chose que des fonctions àApp), verbeux et mal extensible (il faut rajouter tout le code de pattern matching), et sources de bugs (le compilateur aurait vu tout de suite à la compilation qu’il y avait un problème).On peut vouloir dire au compilateur que chaque terme sera évalué à un type particulier, en lui associant un phantom type, sous la forme
data Term a = ... | App (Term a) (Term a). Ainsi à chaque terme est associé un type à la compilation (il est viré à l’exécution). Mais ça ne résout pas nos problèmes, en ayanteval :: Term a -> a, il n’y a pas assez de contraintes surapour que le compilateur empêche un utilisateur d’écrireeval (Intg 123) :: Stringpar exemple (en gros de convertir n’importe comment). La solution c’est d’utiliser les GADTs, qui vont apporter la flexibilité d’écriture nécessaire (le compilateur déduit queeval (Intg n)retourne unInt, et queeval Addretourne unInt->Int->Int), et la sécurité du système de types, en résumant (mal) le manuel d’OCaml :PS : On peut simplifier le code que j’ai donné au dessus, genre avec
eval Add = (+).