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
