### Foralls, Kinds with Arrows, and Impredicativity (?)

I can't figure out why the kinding rule for universal quantification in F_{ω} is:

C, x : k1 |- y : * (1) ----------------------------- C |- (\forall x : k1 . y) : *That is, why the type inside the universal quantification must be of kind

`*`

.
I would expect the rule to be

C, x : k1 |- y : k2 (1') ------------------------------ C |- (\forall x : k1 . y) : k2Using (1), I can still get

C, x : k1 |- y : * -> * (2) ------------------------------------------------------ C |- (\Lambda z : * . \forall x : k1 . y @ z) : * -> *by eta-expansion, so using (1) instead of (1') doesn't seem to reduce the available power, it just makes the notation more annoying.

I suspect that the reason for (1) instead of (1') has something to do with impredicativity, since (1) is only valid in impredicative systems anyway.

## No comments:

Post a Comment