In Types and Programming Languages by Pierce, Ch11 Simple Extensions introduces
λ→ as the simply
typed lambda calculus with simple extensions, and introduces
x (for pair),
List, etc, and calls them "type
Does the following quote from Ch29 on p440 imply that "type constructors" are type operators provided as langauge primitives? (Note that
Refare introduced in Ch13 References not in Ch11, but are also called type constructors. Concept "type operator" is not introduced in Ch11 but until Ch 29
We have also used type-level expressions like
Ref Tinvolving the type constructors
Ref. Although these type constructors are built into the language, rather than being deﬁned by the programmer, they are also a form of functions at the level of types. We can view
Ref, for example, as a function that, for each type T, yields the type of reference cells containing an element of T.
Our task in this and the next two chapters is to treat these type-level func- tions, collectively called type operators, more formally.
Section 30.4 Fragments on
Fωon p461 says that
λ→has no quantification or type operators over proper types.
F1, the only kind is
*and no quantiﬁcation (
∀) or abstraction (
λ) over types is permitted.
F1is just our simply typed lambda-calculus,
λ→. Its deﬁnition is superﬁcially more complicated than Figure 9-1 because it includes kinding and type equivalence relations, but these are both trivial: every syntactically well formed type is also well kinded, with kind
*, and the only type equivalent to a type T is T itself.
λ→ have type operators or not? Do type constructors
λ→ count as type operators?