In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of Fω
30.4.1 Definition: In System F1 , the only kind is
*
and no quantification (∀) or abstraction (λ) over types is permitted.F1 is just our simply typed lambda-calculus,
λ →
. Its definition is super- ficially more complicated than Figure 9-1 because it includes kinding and type equivalence relations, but these are both trivial: every syntactically well formed type is also well kinded, with kind*
, and the only type equivalent to a type T is T itself
Is it correct that quantification ∀
means universal types?
*
is the kind of proper types, which are introduced on p442:
The level of types contains two sorts of expressions. First, there are proper types like Nat, Nat→Nat, Pair Nat Bool, and ∀X.X→X, which are inhabited by terms. (Of course, not all terms have a type; for example (λx:Nat.x) true does not.)
So universal types such as ∀X.X→X
are proper types, and thus belong to kind *
.
Why can System F1 have kind *
, but no universal types, i.e. quantification ∀
?
But if System F1 could have kind *
and quantification ∀
, then wouldn't it become the same as System F2 a.k.a. System F? Quoted from on p461:
In System F2 , we still have only kind
*
and no lambda-abstraction at the level of types, but we allow quantification over proper types (of kind*
).F2 is our System F;
Thanks.