Is `→` a type operator?

Question

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.

Answer 1

Yes, these can all be viewed as operators at the type level, but they're not all completely analogous. Most of these are type constructors in that they're formation operators for types, though type-level application is simply a type operator.

$\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$.