[Haskell-cafe] Re: Higher kinds (and impredicativity?)

[Chung-chieh Shan]

Jim Apple <jbapple+haskell-cafe at gmail.com> wrote in article <ad0e24930701152029n4e6bd254k21c31597730e0054 at 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