Quotient type

Summary

In the field of type theory in computer science, a quotient type is a data type that respects a user-defined equality relation. A quotient type defines an equivalence relation $\equiv$ on elements of the type — for example, we might say that two values of the type Point are equivalent if they have the same respective x- and y-coordinates; formally p1 == p2 if p1.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, if f is a function on values of type Point, it must be the case that for two Points p1 and p2, if p1 == p2 then f(p1) == f(p2).