Foncteurs polymorphes

Foncteurs polymorphes

[Hugo Herbelin]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2971 bytes --]

[ Can we have polymorphism both at function level and at functor level? ]

  Bonjour,

  encore une question sur les modules et le polymorphisme...

  Si j'ai bien compris, il n'y a pas de polymorphisme de foncteur mais
seulement du polymorphisme de fonction. Autrement dit, un foncteur comme

    module Toto (Tutu : sig val f : 'a -> 'a end) = 
    struct
      let tata x = Tutu.f x
      let titi x = Tutu.f [x]
    end

n'est pas polymorphe, seules le sont les fonctions tata et titi, et
chacune de manière indépendante. Autrement dit, en rendant explicite
les quantifications par des variables de type, le type du foncteur est

    module Toto :
      functor(Tutu : sig val f : FORALL 'a. 'a -> 'a end) ->
        sig
          val tata : FORALL 'a. 'a -> 'a
          val titi : FORALL 'a. 'a -> 'a list
        end

où "FORALL 'a." désigne la quantification universelle.


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

  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")


  Intérêt : on peut appliquer Make aussi bien à la structure

    struct let compare = Pervasives.compare end

et obtenir un module polymorphe de type ('a S), qu'à la structure (par exemple)

    struct let compare = (-) end

et obtenir un module polymorphe de type (int S)

  Cela simplifierait aussi le fichier hashtbl de la stdlib, permettant
d'avoir un unique foncteur polymorphe plutôt qu'un foncteur
monomorphe paramétrable par l'égalite + un module polymorphe
forcément basé sur (=).

  Si les foncteurs pouvait être polymorphes, cela compliquerait sans
doute le typage, puisqu'il faudrait sûrement faire de l'unification
pas seulement pour typage des fonctions mais aussi pour le typage
des modules, et qu'il y aurait deux sortes de quantifications des
variables de types des fonctions membres de module.


  Cependant, l'actuelle non-possibilté d'avoir des foncteurs
polymorphes me semble -- naïvement -- d'autant moins impossible que
pour les classes, c'est l'inverse :

  Dans l'exemple suivant, 

    class ('a) toto (f:'a -> 'a) =
      val f=f  
      method tata x = f x
      method titi x = f [x]
    end;;

la quantification est forcément sur la classe, imposant donc le type suivant

    class 'a toto ('a -> 'a) =
      constraint 'a = 'b list
      val f : 'a -> 'a
      method tata : 'a -> 'a
      method titi : 'b -> 'a
    end

où les fonctions ne sont pas indépendamment polymorphes.

                                                  Hugo

Re: Foncteurs polymorphes

[Jerome Vouillon]

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")

Re: Foncteurs polymorphes

[Emmanuel Engel]

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