Quotient type

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In type theory, 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 the cardinality of which is less than or equal to the cardinality 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 carrier 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[edit]