Re: Foncteurs polymorphes

[Emmanuel Engel <Emmanuel.Engel@lri.fr>]

Pour ton probleme de foncteur polymorphe, tu peut trouver une 
partie de la solution dans un de mes precedent messages a la 
mailling liste. Je ne le trouve pas dans l'archive, voici une 
copie de la partie interessante:


:
:
Question:
    Existe-t-il un moyen simple et rapide a l'aide du foncteur 
  Set.Make de creer des ensembles polymorphes qui utilisent une
  fonction de comparaison generique (Pervasives.compare par exemple) ??

  eg 

  module GeneriqueSet = Set.Make(struct ?????? end)

Il me semble que non et, que cette impossibilite est plus due a la facon 
dont est declare le foncteur qui permet de construire les ensembles qu'a 
une vraie limite du systeme; voici une version legerement differente de
ce foncteur qui me permet une telle manip:

module Make(S:sig type 'a t val compare : 'a t -> 'a t -> int end)=
  (struct
     type 'a elt = 'a  S.t
     type 'a set = ('a elt) list
     let empty = []
     and mem = List.mem
     and add e s = e::s
  end:sig
        type 'a elt = 'a S.t
        and 'a set
        val empty : 'a set
        val mem : 'a elt -> 'a set -> bool
        val add : 'a elt -> 'a set -> 'a set
      end);;


module IntSet = Make(struct type 'a t = int let compare = (compare:int
-> int -> int) end);;
module GenericSet = Make(struct type 'a t = 'a let compare = compare
end);;


------- fin du message

Je suis bien d'accord que cette version, meme si elle permet un peut
plus
de liberte que le version actuelle n'est pas aussi generale que des
foncteurs 
"polymorphes". Par exemple, je ne peut pas definir

module PSet = Make(struct type ('a,'b)t = 'a * 'b let compare (x,_)
(y,_) = compare x y end);;

alors qu'avec l'extension que tu propose cela serait a prioris possible.
Toutefois 
il me semble que de serieux problemes se profillent a l'horizon avec une 
telle extension; en ocaml les foncteurs sont d'ordre superieur et tu
veut pouvoir
lier les variables a n'importe quel niveaux. Cela ressemble furieusement
au systeme F. 
Et la je ne suit meme pas sur que le sous typage sous decidable (ie
decider si F(X) 
est valide implique de verifier F : S1 -> S2, X : S3 et S1 <: S3 ).
                                                        ^^^^^^^^
 
-- 

- Emmanuel Engel