Re: Module et type abstrait

Pour ce cas, ça doit pouvoir se faire avec des GADT

Cela dépend beaucoup ce que tu entends par "ce cas" et pouvoir se faire:
il est possible d'encoder les entiers naturels dans le système de type d'OCaml, avec des GADTs ou des types fantômes; cependant la complexité de l'encodage a tendance à s'accroître rapidement avec l'expressivité dudit encodage.

Par exemple, l'encodage le plus simple

 type z = private Z
 type 'a succ = private Succ
 type 'nat t = Z: z t | S: 'nat t -> 'nat succ t

fonctionne mais à plusieurs limitations majeures:

• la taille du type augmente linéairement avec l'entier, ce qui peut créer des problèmes pour le compilateur assez rapidement ( il avait tendance à planter vers 65000 lors de mes derniers tests? )

• les opérations que l'on peut effectuer sont très limitées.

Mais il peut être suffisant pour encoder un certain nombre d'invariants en algèbre linéaire (par exemple, on peut vérifier que les dimensions des matrices dans le produit matriciel soient correctes). Par contre, si je souhaite concaténer deux vecteurs, j'aurai
besoin d'encoder l'addition d'entier dans mon type 'nat1 t -> 'nat2 t -> ('nat1 + 'nat2) t?

Cependant, avec cet encodage, le système de type n'a pas assez d'information pour construire le type 'nat1 + 'nat2, il faut soit passer par des types auxiliaires, ou modifier l'encodage des entiers. Un exemple qui marche est d'encoder des propositions
de la forme a + b = c:

 type 'nat t = 
 | Z: ('a*'a) t (* 'a + z = 'a*) 
 | S: ('z,'a) t -> ('z,'a succ) t (* si 'n + a = b alors 'n + succ a = succ b *)

À partir de cet encodage, on peut écrire l'addition

 let add: type inf mid sup: (inf * mid) nat -> (mid * sup) nat -> (inf * sup) nat =
 fun a b -> match b with
 | Z -> a
 | S n -> S (add a n)

Cependant, le paramètre de type libre 'a a tendance à créer des problèmes du au fait que le GADT n'est pas covariant, donc la relaxed value restriction ne s'applique plus et
il est très (trop) facile de se retrouver avec des types faibles.

Et la complexité ne fait qu'empirer si on essaie d'implémenter d'autres fonctionnalités (représentation binaire, multiplication, comparaison, etc ...) sur les entiers dans le système de types.

Un bon exemple de ce qui peut être fait raisonnablement dans le cadre de l'algèbre linéaire est SLAP.

Un exemple pédagogique pour montrer à quel point le budget de complexité peut exploser facilement serait ma bibliothèque expérimentale tensority.