Re: Foncteurs polymorphes

[Jerome Vouillon <vouillon@clipper.ens.fr>]

On Mon, 25 Aug 1997, Hugo Herbelin wrote:

> Cela tient-il la route d'avoir une notion de polymorphisme dans les
> modules qui soit distincte du polymophisme des fonctions qu'il
> contient.

Cela a effectivement un sens, et a d'ailleurs ete deja propose par
Stefan Kahrs (http://www.dcs.ed.ac.uk/home/smk/).

Cependant, pour assurer la correction du typage en presence d'effets
de bords, la technique utilisee par O'caml est de ne generaliser le
type que des expressions qui sont syntaxiquement des valeurs (toutes
les autres techniques compliquent le systeme de type). La quantifi-
cation du type des modules perd beaucoup de son interet si l'on
generalise cette technique aux expressions de module. Ainsi, dans ton
exemple, le module defini par
   module M = Make(struct let compare = Pervasives.compare end)
aurait le type '_a S et non 'a S. En particulier, le type de M.empty
est '_a t, qui n'est pas polymorphe.

-- Jerome Vouillon

>   Exemple pratique : le foncteur Set.Make.
> 
>   Pourrait-on avoir les types suivants pour le module Set :
> 
>     module type 'a OrderedType =
>       sig
>         val compare: 'a -> 'a -> int
>       end
> 
>     module type 'a S =
>       sig
>         type 'a t
>         val empty: 'a t
>         ...
>      end
> 
>     module Make(Ord: 'a OrderedType) : 'a S
> 
> où la quantification par 'a est maintenant sur Make (i.e. Make a le
> type explicitement quantifié "FORALL 'a. 'a OrderedType -> 'a S")