Alexei Kopylov.
Dependent Intersection: A New Way of Defining Records in Type Theory.
Technical Report TR2000-1809, Computer Science Department, Cornell University, August 2000
Submited to LICS'03.
Records and dependent records are a powerful tool for programming, representing
mathematical concepts, and program verification. In the last decade several type systems with records as primitive types were
proposed. The question is arose: whether it is possible to define record type in
existent type theories using standard types without introducing new primitives.
It was known that independent records can be defined in type theories with dependent functions or
intersection. On the other hand dependent records cannot be formed using standard types.
Hickey introduced a complex notion of very dependent functions to
represent dependent records. In the current paper we extend Martin-Löf's type theory with a simpler type constructor
dependent intersection, i.e., the intersection of two types, where the second type may depend on elements of the first one
(not to be confused with the intersection of a family of types). This new type constructor allows us to define dependent records
in a very simple way. It also allows us to define the set type constructor.
Key words:
type theory, record, dependent records, abstract data type, intersection