[Caml-list] First-class module and higher-order types

[Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr>]

[-- Attachment #1: Type: text/plain, Size: 1199 bytes --]

Dear all,

One way to use first-class module is to "extend" a functor without resorting
to a new functor. Like, for instance:

type ('a,'t) set = (module Set.S with type elt = 'a and type t = 't)

let add2 (type a) (type t) (m:(a,t) set) x y s =
   let module S = (val m:Set.S with type elt = a and type t = t) in
   S.add x (S.add y s);;

But if that works pretty with Set, it won't work with Map for two reasons.
One is that syntax won't allow us to write something like

with 'a t = …

in the type constraints. Another, probably more serious, is that there is no
equivalent to (type t), for type families ( (type 'a t) ?).


Now that would be a pretty useful thing to do, in some case. Hence I have a
twofold question:


   1. On the practical side, does anyone knows a workaround ? Could I find a
   way to extend Map without a functor if I'm tricky?
   2. On the theoretical side, how hard is it to design a variant of
   Hindley-Milner's typing algorithm with type-family quantification? (I
   understand that Ocaml's typing machinery is pretty hard to change, and that
   it will most likely not be happening any time soon in practice)


--
Arnaud Spiwack

[-- Attachment #2: Type: text/html, Size: 1989 bytes --]