[Caml-list] Question on typing

[Caml-list] Question on typing

[Christian RINDERKNECHT]

Dear list members,

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};;

I suspect non-decidability of type inference (higher-order
unification), but I am not an expert of that topic. Also, is type
verification undecidable? Is it due to functional types? What happen
is there is no (value) functions?

Best regards,

-- 

Christian

-----------------------------------------------------------------------
Christian Rinderknecht                     Phone +33 (0)1 60 76 44 43
Institut National des Télécommunications   Fax   +33 (0)1 60 76 47 11
Département Logiciels Réseaux (LOR)        WWW
9, Rue Charles Fourier, F-91011 Évry Cedex
-------------------
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

Re: [Caml-list] Question on typing

[Xavier Leroy]

> 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

Re: [Caml-list] Question on typing

[Andreas Rossberg]

Christian RINDERKNECHT wrote:
> 
> 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;;

[Longish and technical answer, summary follows below.]

What you want is usually refered to as higher-order polymorphism. There
are two reasons against having it in the language, one pragmatical, the
other technical.

First, if you wanted to allow this you had to introduce a proper `kind'
system into the language. Kinds are the "types of types". For example,
int has kind * (which denotes ground types), while eg. the list type
constructor has kind *->* (a type function from ground types to ground
types). Types with kind other than * are usually called constructors in
type theory.

Ocaml restricts constructors to have first-order kinds, ie. kinds of the
form *->*->*->* etc. (well, actually it does not use currying but rather
has tuple kinds, but that does not make much of a difference). The
constructor t you want to declare has kind (*->*)->*, however, ie. it is
higher-order. Another important restriction in Ocaml is that
constructors may only be used with a full supply of arguments. You would
bump into this second restriction with your example as soon as you
actually tried to apply t: you cannot write down any type expression of
kind *->*.

The point with both these restrictions is that you do not need to
declare kinds for type variables. Any type variable has kind * and the
programmer need not be bothered with kinds. If you wanted to lift the
restrictions you either had to introduce syntax for kinds in the
language and annotate type variables at their binding occurance, or you
had to do `kind inference'.

The second argument against higher-order polymorphism in ML is that -
without at least some restrictions - it would indeed require
higher-order unification for type inference, because conceptually you
get arbitrary lambdas at the type level. Higher-order unification is
undecidable. So undecidability is due to functional kinds (ie. functions
at the type level), it has nothing to do with functional types
(functions at the value level) as you suspected.

However, there are in fact languages that provide higher-order
polymorphism, Haskell being one example. Haskell deals with the
pragmatic side by doing kind inference. For your example it is easy to
derive that 'a has kind *->*. But there are examples where no unique
kind can be infered. Consider

	type ('a,'b) apply = 'b 'a

Apply can have any kind of the form (K->K')->K->K'. So if you do not
want to introduce kind syntax into the language you can either have
`polymorphic kinds' (which further complicates things) or you have to do
some defaulting. This is what Haskell does, assigning * whenever there
is no more information available. This seems to work pretty well in
practice but of course precludes a lot of useful higher-order type
definitions. Moreover, the inference approach does not work for the
specification of abstract types in ML signatures.

The decidability problem is dealt with by restricting the use of type
synonyms: a type constructor that is not generative (ie. just
abbreviates some type) may still only be used fully applied. This avoids
type lambdas during type inference (there remain only constants and
variables of higher kind) and unification stays decidable. Of course, it
also precludes useful examples: You could write

	type u = list t

because list is a generative constructor (a constant), but not

	type 'a aux = 'a * 'a
	type v = aux t

because aux is a type synonym that is not used in a fully applied
fashion in the definition of v.

(BTW, ML's choice of postfix syntax and tupled arguments for type
application is really unfortunate when you want to extend it to
higher-order types. :-( )

So you still need some restrictions. Those could only be lifted if you
did not care for inference: type checking alone, where you provide full
type and kind annotations at lambda bindings, is decidable, because you
essentially get the higher-order lambda calculus.

To summarise: it can be done but significantly complicates the language
and requires some restrictions to maintain decidable type inference.
YMMV whether the additional degree of genericity is worth this
complication, in particular since most of it can be done in ML via
modules already.

BTW, your second type declaration

> type 'a t = {x : 'a 'a};;

is ill-kinded, very much like the value declaration

	let t a = {x = a a}

is ill-typed - unless you introduce something as esoteric as recursive
kinds ;-)

Best regards,

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids.
 If Pac Man affected us as kids, we would all be running around in
 darkened rooms, munching pills, and listening to repetitive music."
-------------------
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