Abstract
In the most general sense, dependent types are type-valued functions. This
definition includes, for example, the type operators of Fω such as Pair. When
applied to two types S and T, this yields the type Pair S T whose elements
are pairs (s, t) of elements s from S and t from T (see TAPL, Chapter 29).
However, the terminology “dependent types” is usually used to indicate a
particular class of type-valued functions: those functions which send terms
to types. In this chapter we study this kind of dependency.
| Original language | English |
|---|---|
| Title of host publication | Advanced Topics in Types and Programming Languages |
| Editors | Benjamin C. Pierce |
| Publisher | MIT Press |
| Pages | 45-86 |
| Number of pages | 42 |
| ISBN (Electronic) | 9780262332668 |
| ISBN (Print) | 9780262162289 |
| Publication status | Published - Dec 2004 |