Quotient_type
Quotient type
Data type in type theory
In the field of type theory in computer science, a quotient type is a data type which respects a user-defined equality relation. A quotient type defines an equivalence relation on elements of the type - for example, we might say that two values of the type Person
are equivalent if they have the same name; formally p1 == p2
if p1.name == p2.name
. In type theories which allow quotient types, an additional requirement is made that all operations must respect the equivalence between elements. For example, if f
is a function on values of type Person
, it must be the case that for two Person
s p1
and p2
, if p1 == p2
then f(p1) == f(p2)
.
Quotient types are part of a general class of types known as algebraic data types. In the early 1980s, quotient types were defined and implemented as part of the Nuprl proof assistant, in work led by Robert L. Constable and others.[1][2] Quotient types have been studied in the context of Martin-Löf type theory,[3] dependent type theory,[4] higher-order logic,[5] and homotopy type theory.[6]