Book contents
- Frontmatter
- Contents
- Preface
- Notation
- 1 Continuity and computability
- 2 Syntactic theory of the λ-calculus
- 3 D∞ models and intersection types
- 4 Interpretation of λ-calculi in CCC's
- 5 CCC's of algebraic dcpo's
- 6 The Language PCF
- 7 Domain equations
- 8 Values and computations
- 9 Powerdomains
- 10 Stone duality
- 11 Dependent and second order types
- 12 Stability
- 13 Towards linear logic
- 14 Sequentially
- 15 Domains and realizability
- 16 Functions and processes
- Appendix 1 Summary of recursion theory
- Appendix 2 Summary of category theory
- References and bibliography
- Index
11 - Dependent and second order types
Published online by Cambridge University Press: 05 November 2011
- Frontmatter
- Contents
- Preface
- Notation
- 1 Continuity and computability
- 2 Syntactic theory of the λ-calculus
- 3 D∞ models and intersection types
- 4 Interpretation of λ-calculi in CCC's
- 5 CCC's of algebraic dcpo's
- 6 The Language PCF
- 7 Domain equations
- 8 Values and computations
- 9 Powerdomains
- 10 Stone duality
- 11 Dependent and second order types
- 12 Stability
- 13 Towards linear logic
- 14 Sequentially
- 15 Domains and realizability
- 16 Functions and processes
- Appendix 1 Summary of recursion theory
- Appendix 2 Summary of category theory
- References and bibliography
- Index
Summary
The main goal of this chapter is to introduce λ-calculi with dependent and second order types, to discuss their interpretation in the framework of traditional domain theory (chapter 15 will mention another approach based on realizability), and to present some of their relevant syntactic properties.
Calculi with dependent and second order types are rather complex syntactic objects. In order to master some of their complexity let us start with a discussion from a semantic viewpoint. Let T be a category whose objects are regarded as types. The category T contains atomic types like the singleton type 1, the type nat representing natural numbers, and the type bool representing boolean values. The collection T is also closed with respect to certain data type constructions. For example, if A and B are types then we can form new types such as a product type A × B, a sum type A + B, and an exponent type A → B.
In first approximation, a dependent type is a family of types indexed over another type A. We represent such a family as a transformation F from A into the collection of types T, say F : A → T. As an example of dependent type we can think of a family Prod. bool: nat → T that given a number n returns the type bool × … × bool (n times).
- Type
- Chapter
- Information
- Domains and Lambda-Calculi , pp. 240 - 269Publisher: Cambridge University PressPrint publication year: 1998