In the field oftype theory incomputer science, aquotient type is adata type that respects a user-definedequality relation. A quotient type defines anequivalence relation${\displaystyle \equiv }$ on elements of the type — for example, we might say that two values of the typePoint are equivalent if they have the same respective x- and y-coordinates; formallyp1 == p2 ifp1.x == p2.x && p1.y == p2.y. In type theories that allow quotient types, an additional requirement is made that all operations must respect the equivalence between elements. For example, iff is a function on values of typePoint, it must be the case that for twoPointsp1 andp2, ifp1 == p2 thenf(p1) == f(p2).

Quotient types are part of a general class of types known asalgebraic data types. In the early 1980s, quotient types were defined and implemented as part of theNuprlproof assistant, in work led byRobert L. Constable and others.^[1][2] Quotient types have been studied in the context ofMartin-Löf type theory,^[3]dependent type theory,^[4]higher-order logic,^[5] andhomotopy type theory.^[6]

To define a quotient type, one typically provides adata type together with anequivalence relation on that type, for example,Point // ==, where== is a user-defined equality relation. The elements of the quotient type areequivalence classes of elements of the original type.^[3]

Quotient types can be used to definemodular arithmetic. For example, ifInteger is a data type of integers,${\displaystyle {\equiv }_2}$ can be defined by saying that${\displaystyle x{\equiv }_{2}y}$ if the difference${\displaystyle x-y}$ is even. We then form the type of integers modulo 2:^[1]

Integer //${\displaystyle {\equiv }_2}$

The operations on integers,+,- can be proven to be well-defined on the new quotient type.

In type theories that lack quotient types,setoids (sets explicitly equipped with an equivalence relation) are often used instead of quotient types. However, unlike with setoids, many type theories may require aformal proof that any functions defined on quotient types arewell-defined.^[7]

Quotient types are part of a general class of types known asalgebraic data types. Just asproduct types andsum types are analogous to the cartesian product and disjoint union of abstract algebraic structures, quotient types reflect the concept of set-theoreticquotients, sets whose elements are partitioned intoequivalence classes by a given equivalence relation on the set. Algebraic structures whoseunderlying set is a quotient are also termed quotients. Examples of such quotient structures include quotientsets,groups,rings,categories and, in topology,quotient spaces.^[3]

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

• Data types
• Type theory
• Composite data types

• Articles with short description
• Short description is different from Wikidata