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

2011-08-20 Thread 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



--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

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

2011-08-19 Thread Arnaud Spiwack 
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

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs