# Is → a type operator?

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.

$$\to$$ may be viewed as an ordinary type constructor. In Pierce's notation, this is denoted $$\lambda X . \lambda Y . X \to Y$$. You can just as well think of it as binary algebraic structure on the set of types $$(-) \to (-) : \star, \star \to \star$$, where $$\star$$ is the kind of types. (If you have a higher kind above this, it could live there, but this depends on precisely what your calculus is.) The product of types, $$\times$$, may be viewed similarly. Type-level application is also a type operator.
$$\forall X$$, $$\exists X$$ and $$\lambda X$$ are also type constructors, but they're a little different from the previous two in that they're binding operators: just like the $$\lambda$$ term operator, they bind a variable in the context (though in this case, a type variable). This means these type constructors are no longer algebraic operators à la universal algebra like the simple type constructors $$\to$$ and $$\times$$.