[Camllist] Question on typing

Christian RINDERKNECHT
 Xavier Leroy
 Andreas Rossberg
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Andreas Rossberg <rossberg@p...> 
Subject:  Re: [Camllist] Question on typing 
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 higherorder 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 firstorder 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 higherorder. 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 higherorder polymorphism in ML is that  without at least some restrictions  it would indeed require higherorder unification for type inference, because conceptually you get arbitrary lambdas at the type level. Higherorder 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 higherorder 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 higherorder 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 higherorder 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 higherorder 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 illkinded, very much like the value declaration let t a = {x = a a} is illtyped  unless you introduce something as esoteric as recursive kinds ;) Best regards,  Andreas  Andreas Rossberg, rossberg@ps.unisb.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/camlbugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr