| The new Haskell report 1.3 (preliminary) allows type variables of
| other kinds than *, e.g. it gives the example (page 51)
|
| data App f a = A (f a)
|
| where the type variable f has kind *->*, and App has (*->*)->*->*.
|
| My problem is that I haven't seen (in the report) any mention
| about the interaction of this with type inference.
|
| Take for instance the declaration:
| something = A ()
| what is the type of something ?
| It could be App (\x->x) (), but it could also be
| App (\x->()) a, for any type a, and a few others.
No, in fact there is only possibility for this definition of "something"
in Haskell 1.3; a type error. There are no lambda expressions in Haskell
types, just variables, constants, and applications. There is no way,
in the type language of Haskell 1.3 at least, to unify the constant ()
with the application (f a).
The report does contain a pointer to my paper on constructor classes in
FPCA 93 where the formal treatment of unification and type inference is
explained (But perhaps that reference should be changed to point to the
expanded version of the paper, which appeared in the Journal of Functional
Programming, Volume 5, Part 1, Pages 1--36).
| But these are different types and it matters for type inference which
| one we choose, there is no longer a most general type, a principal type.
| Basically, these are the usual problems with higher-order unification
| (including that it's undecidable).
The basic Haskell 1.3 type system is decidable and has principal types.
In other words, there is an effective type inference algorithm that
produces a most general type for any well-typed program, and fails
if no such typing exists.
All the best,
Mark
