Quotient type

In type theory, a kind of foundation of mathematics, a quotient type is an algebraic data type that represents a type whose equality relation has been redefined by a given equivalence relation such that the elements of the type are partitioned into a set of equivalence classes whose cardinality is less than or equal to that of the base type. Just as product types and sum types are analogous to the cartesian product and disjoint sum of abstract algebraic structures, quotient types reflect the concept of set-theoretic quotients, sets whose elements are surjectively partitioned into equivalence classes by a given equivalence relation on the set. Algebraic structures whose underlying set is a quotient are also termed quotients. Examples of such quotient structures include quotient sets, groups, rings, categories and, in topology, quotient spaces. For example, $\mathbb{Q}$, the rational numbers, is the quotient ring – or "field of fractions" – of $\mathbb{Z}$, the integers.

In type theories that lack quotient types, setoids – sets explicitly equipped with an equivalence relation – are often used instead.

See also

• Algebraic data type
• Product type
• Sum type
• Setoid