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.
|Title of host publication||Advanced Topics in Types and Programming Languages|
|Editors||Benjamin C. Pierce|
|Number of pages||42|
|Publication status||Published - Dec 2004|