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)



Your Answer

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

Browse other questions tagged or ask your own question.