Jim Apple <jbapple+haskell-cafe@gmail.com> wrote in article <ad0e24930701152029n4e6bd254k21c31597730e0054@mail.gmail.com> in gmane.comp.lang.haskell.cafe:
(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