Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire
Je pensais effectivement à l'encodage sous la forme des entiers de Peano. Comme c'est une représentation unaire des entiers, leur taille croît bien linéairement. C'est aussi cet encodage qui est illustré dans le cours de Jeremy Yallop.
L'idée est bien de montrer qu'avec les GADT, on peut avoir une forme affaiblie de type dépendant. Pour avoir des types dépendants complets, il faut passer à des langages comme Coq; mais là, c'est pour les fous ! :-P
Merci pour les deux liens, je regarderai cela à tête reposée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Module et type abstrait
Posté par kantien . En réponse au journal Une petite histoire d'utilisation type fort dans Ocaml. Évalué à 3.
Je pensais effectivement à l'encodage sous la forme des entiers de Peano. Comme c'est une représentation unaire des entiers, leur taille croît bien linéairement. C'est aussi cet encodage qui est illustré dans le cours de Jeremy Yallop.
L'idée est bien de montrer qu'avec les GADT, on peut avoir une forme affaiblie de type dépendant. Pour avoir des types dépendants complets, il faut passer à des langages comme Coq; mais là, c'est pour les fous ! :-P
Merci pour les deux liens, je regarderai cela à tête reposée.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.