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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2011/08/20, at 0:38, Arnaud Spiwack wrote:

> 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:
> 
> 	• On the practical side, does anyone knows a workaround ? Could I find a way to extend Map without a functor if I'm tricky?

Basically, you need to monomorphize the map module.
You can either do it by hand, rewriting the signature completely, or use some conversion functions:

module type MapT = sig
  include Map.S
  type data
  type map
  val of_t : data t -> map
  val to_t : map -> data t
end

type ('k,'d,'m) map =
    (module MapT with type key = 'k and type data = 'd and type map = 'm)

let add (type k) (type d) (type m) (m:(k,d,m) map) x y s =
   let module M =
     (val m:MapT with type key = k and type data = d and type map = m) in
   M.of_t (M.add x y (M.to_t s))

module SSMap = struct
  include Map.Make(String)
  type data = string
  type map = data t
  let of_t x = x
  let to_t x = x
end

let ssmap =
  (module SSMap:
   MapT with type key = string and type data = string and type map = SSMap.map)
;;

add ssmap;;

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

Well, Haskell has higher-order type constructors, but its type system is much less structural.
In particular, I have no idea how this would interact with recursive types.

Jacques Garrigue