0
$\begingroup$

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.

$\endgroup$

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.