15 Jan
2007
15 Jan
'07
11:29 p.m.
On 1/15/07, Chung-chieh Shan
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