Foncteurs polymorphes

[Hugo Herbelin <herbelin@margaux.inria.fr>]

[-- 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