Jim Apple
(forall (f :: * -> *) . f) Int. What values inhabit this type?
The same ones that inhabit (forall (f :: * -> *) . f Int); that is, none (or _|_). I don't see the uninhabitability of a type as reason why the type itself should be ill-formed, even in a domain without lifted types.
I'm sorry I wasn't clear; I did not mean to argue that a type should be ill-formed just because it is not inhabited. Let me try to say something else. The kind system should be to types as the type system is to terms; in particular, if a type is well-kinded (i.e., well-formed) then it should either be a "value type" (such as "[Int]" and "forall a. a") or contain a redex (such as "(\a -> a) Int"). The proposed type above is neither; it is stuck just as the program "1 + \x->x" is stuck. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig