In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of

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;



Why can System F1 have kind *, but no universal types, i.e. quantification ∀?

Because "System F1 has types of kind *" does not mean "any types which have kind * in some other system (e.g. universal types) are allowed in F1".

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.