Module

Type.Quotient

Approximation of quotient types.

class Canonical a e | e -> a where

Equivalence relation disguised as a canonicalization function.

newtype Quotient a e

Quotient type with equivalence relation e. The runtime representation is identical to that of a.

Operator alias for Type.Quotient.Quotient (left-associative / precedence 9)

mkQuotient :: forall e a. a -> a / e

Pair a value with an equivalence relation.

runQuotient :: forall e a. Canonical a e => a / e -> a

Canonicalize a value using an equivalence relation such that the caller cannot observe distinct wrappees.

data Id :: Type

T / Id ~ T.

data Abs :: Type

Negative values are equivalent to their positive counterparts.

data Mod :: Nat1 -> Type

Integers modulo some positive number.