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

[Chung-chieh Shan]

Jim Apple <jbapple+haskell-cafe at gmail.com> wrote in article <ad0e24930701141839r65423008pb7f7c8b3e95073db at mail.gmail.com> in gmane.comp.lang.haskell.cafe:
> 
> C, x : k1 |- y : *
> -----------------------
> C |- (\forall x : k1 . y) : *
> 
> I'd expect
> 
> C, x : k1 |- y : k2
> -----------------------
> C |- (\forall x : k1 . y) : k2
> 
> Is there a foundational or an implementation reason for this restriction?

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?

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
My mother is a fish.