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

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

[Arnaud Spiwack]

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

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

[Jacques Garrigue]

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

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

[Andreas Rossberg]

On Aug 20, 2011, at 05.26 h, Jacques Garrigue wrote:
> On 2011/08/20, at 0:38, Arnaud Spiwack wrote:
>> 	• 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.

Interesting. I'm curious. The essential restriction in Haskell is that  
universally quantified type variables of non-trivial kind can only be  
instantiated with nominal type constructors (in order to avoid the  
need for higher-order unification).  Shouldn't the same work for OCaml?

Or are you referring to type normalisation for (explicit) applications  
of higher-order type constructors? Given that OCaml only allows equi- 
recursion at base kind, how could it interact in interesting ways?

Thanks,
/Andreas