Higher kinds (and impredicativity?)
Why is this declaration ill-formed: data Bad t where Bad :: Bad (forall (f :: * -> *) . f) GHC 6.6 says: `f' is not applied to enough type arguments Expected kind `*', but `f' has kind `* -> *' In the type `forall f :: (* -> *). f' In the type `Bad (forall f :: (* -> *). f)' In the data type declaration for `Bad' I suppose this is because the kind inference rule is 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? Jim
Jim Apple
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.
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
Jim Apple
(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
On 1/16/07, Chung-chieh Shan
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").
I think I see. I was expecting that (forall v : k . t)@s could beta-reduce to (forall v : k . t@s), which in retrospect seems greedy. :-) Thanks, Jim
participants (2)
-
Chung-chieh Shan -
Jim Apple