Quotient type

Short description: 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]

## Contents

* 1 Definition
* 2 Variations
* 3 Properties
* 4 References
* 5 See also

## Definition

To define a quotient type, one typically provides a data type together with an equivalence relation on that type, for example, `Person // ==`, where `==` is a user-defined equality relation. The elements of the quotient type are equivalence classes of elements of the original type.[3]

Quotient types can be used to define modular arithmetic. For example, if `Integer` is a data type of integers, ≡2 can be defined by saying that x≡2y if the difference x−y is even. We then form the type of integers modulo 2:[1]

`Integer //` ≡2

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

## Variations

In type theories that lack quotient types, setoids \- sets explicitly equipped with an equivalence relation –= are often used instead. However, unlike with setoids, many type theories may require a formal proof that any functions defined on quotient types are well-defined.[7]

## Properties

Quotient types are part of a general class of types known as algebraic data types. Just as product types and sum types are analogous to the cartesian product and disjoint union of abstract algebraic structures, quotient types reflect the concept of set-theoretic quotients, sets whose elements are 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.[3]

## References

1. ↑ 1.0 1.1 Constable, Robert L. (1986) (in en). Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall. ISBN 978-0-13-451832-9. https://books.google.com/books?id=Z4OzAAAAIAAJ.
2. ↑ Constable, R. L. (1984). "Mathematics as programming". in Clarke, Edmund; Kozen, Dexter (in en). Lecture Notes in Computer Science. 164. Berlin, Heidelberg: Springer. 116–128. doi:10.1007/3-540-12896-4_359. ISBN 978-3-540-38775-6. https://link.springer.com/chapter/10.1007/3-540-12896-4_359.
3. ↑ 3.0 3.1 3.2 Li, Nuo (2015-07-15). "Quotient types in type theory" (in en). https://eprints.nottingham.ac.uk/28941/.
4. ↑ Hofmann, Martin (1995). "A simple model for quotient types" (in en). Lecture Notes in Computer Science. 902. Berlin, Heidelberg: Springer. 216–234. doi:10.1007/BFb0014055. ISBN 978-3-540-49178-1. https://link.springer.com/chapter/10.1007/BFb0014055.
5. ↑ Homeier, Peter V. (2005). "A Design Structure for Higher Order Quotients". in Hurd, Joe; Melham, Tom (in en). Lecture Notes in Computer Science. 3603. Berlin, Heidelberg: Springer. 130–146. doi:10.1007/11541868_9. ISBN 978-3-540-31820-0. https://link.springer.com/chapter/10.1007/11541868_9.
6. ↑ "The HoTT Book" (in en). 2013-03-12. https://homotopytypetheory.org/book/.
7. ↑ Hofmann, Martin (1997). "Extensional Constructs in Intensional Type Theory" (in en). SpringerLink. doi:10.1007/978-1-4471-0963-1. ISBN 978-1-4471-1243-3. https://link.springer.com/book/10.1007/978-1-4471-0963-1.

## See also

* Algebraic data type
* Product type
* Setoid
* Sum type

* v
* t
* e

Data types

Uninterpreted|

* Bit
* Byte
* Trit
* Tryte
* Word
* Bit array

Numeric|

* Arbitrary-precision or bignum
* Complex
* Decimal
* Fixed point
* Floating point
* Double precision
* Extended precision
* Long double
* Octuple precision
* Quadruple precision
* Single precision
* Reduced precision
* Minifloat
* Half precision
* bfloat16
* Integer
* signedness
* Interval
* Rational

Pointer|

* Address
* physical
* virtual
* Reference

Text|

* Character
* String
* null-terminated

Composite|

* Algebraic data type
* generalized
* Array
* Associative array
* Class
* Dependent
* Equality
* Inductive
* Intersection
* List
* Object
* metaobject
* Option type
* Product
* Record or Struct
* Refinement
* Set
* Union
* tagged

Other|

* Boolean
* Bottom type
* Collection
* Enumerated type
* Exception
* Function type
* Opaque data type
* Recursive data type
* Semaphore
* Stream
* Top type
* Type class
* Unit type
* Void

Related
topics|

* Abstract data type
* Data structure
* Generic
* Kind
* metaclass
* Parametric polymorphism
* Primitive data type
* Protocol
* interface
* Subtyping
* Type constructor
* Type conversion
* Type system
* Type theory

See also platform-dependent and independent units of information

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Quotient type. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Quotient_type&oldid=219784"
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template