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 constructors".

  1. Does the following quote from Ch29 on p440 imply that "type constructors" are type operators provided as langauge primitives? (Note that Array and Ref are 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 Array T and Ref T involving the type constructors Array and Ref. Although these type constructors are built into the language, rather than being defined 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.

  2. Section 30.4 Fragments on on p461 says that λ→ is F1, because λ→ has no quantification or type operators over proper types.

    In System F1 , the only kind is * and no quantification () or abstraction (λ) over types is permitted.

    F1 is just our simply typed lambda-calculus, λ→ . Its definition is superficially 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.

Does λ→ have type operators or not? Do type constructors x and List in λ→ count as type operators?

Is λ→ system F1?



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.