[Haskell-cafe] Re: Higher kinds (and impredicativity?)
jbapple+haskell-cafe at gmail.com
Mon Jan 15 23:29:42 EST 2007
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.
More information about the Haskell-Cafe