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

[Andreas Rossberg <rossberg@mpi-sws.org>]

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