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

[Jim Apple]

On 1/15/07, Chung-chieh Shan <ccshan at post.harvard.edu> wrote:
> I consider it a foundational reason.  You seem to want
>
>     (forall (f :: * -> *) . f)
>
> to have kind
>
>     * -> *.
>
> But that means that I should be able to apply it to a type, say Int, to
> get a type
>
>     (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. For instance, (Int -> (forall a . a)) should be a valid
type even in a system where it is not inhabited, because I want to be
able to write the type ((Int -> (forall a . a)) -> (forall b . b)),
which is inhabited.

Jim