Relating types
This chapter collects three tools for working with types:
-
Type classes let shared structure across types be organized into hierarchies.
-
Quotient types encode equivalence classes by identifying expressions under an equivalence relation.
-
Coercions encode embeddings between types, and more generally, let expressions of one type be used implicitly where another is expected.
Type classes underpin the other two: quotient types are formed from instances of the Setoid type class, and coercions are implemented as type class instances at the elaboration stage. Type classes are inductive types with special elaboration-level features, so they require no new kernel-level primitives. Quotient types, by contrast, come with a number of primitives for their formation, the introduction and elimination of quotient expressions, and reasoning about them.