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 |