In Types and Programming Languages by Pierce,
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.)
Then there are type operators like Pair and λX.X→X, which do not them- selves classify terms (it does not make sense to ask “What terms have type λX.X→X?”), but which can be applied to type arguments to form proper types like (λX.X→X)Nat that do classify terms.
Is →
a type operator? →
seems to me to take two types as arguments and return a function type.
Does it belong to some kind?
I might miss it, but does TAPL say anything about it?
Similar questions for
x
(for pairing two types, e.g.T1 x T2
, c.f. Ch11).∀X.
in universal type∀X.T
in Figure 23-1 of Ch23 on p343{∃X,}
in existential type{∃X,T}
in Figure 24-1 of Ch24 p366λX:: .
in type operator abstractionλX::K.S
(c.f. Figure 29-1 in Ch29 on p446)Space
in type operator application
T1 T2
(c.f. Figure 29-1 in Ch29 on p446)
Thanks.