Re: [Caml-list] Question on typing

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> I have a question about typing, but which is not uniquely related to
> Caml. 
> Could someone tell me the reason why a type variable cannot be used as
> a type constructor, like in:
> 
> type 'a t = K of bool 'a;;
> 
> or
> 
> type 'a t = {x : 'a 'a};;

The latter is ill-sorted :-)  

> I suspect non-decidability of type inference (higher-order
> unification), but I am not an expert of that topic. Also, is type
> verification undecidable?

Type verification is decidable and not difficult; you basically get
the type system known as F_omega, which is contained as a subset in
all higher-order logical frameworks such as Coq, as well as in
Cardelli's experimental language Quest from the late 80s.

As for type inference, one could indeed fear that it involves
(undecidable) higher-order unification.  I seem to remember that it
does not, actually -- at least in the situation you outline above,
i.e. with explicit declarations of type constructors.  I'm away from
my big file of research papers at INRIA, but I believe these ideas
have been explored in Haskell ("constructor classes"), in particular
by Mark Jones, and found to be quite tractable.

- Xavier Leroy
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr