Newtype.Union

Documentation

module Data.Type.Coercion.Related

data IsUnion x y z

IsUnion x y z witnesses the fact:

• All x, y, z share the same runtime representation
• z is a union type of x and y. In other words, the following three holds:

• Sub x z

• Sub y z

• For any type r satisfying both of (Sub x r, Sub y r), Sub z r.

Constructors

IsUnion

Fields

• inl :: !(Sub x z)

  x can be safely coerced to z

• inr :: !(Sub y z)

  y can be safely coerced to z

• elim :: forall r. Sub x r -> Sub y r -> Sub z r

  Given both x and y can be safely coerced to r, too z can.

Instances

TestCoercion (IsUnion x y :: Type -> Type)

Defined in Newtype.Union

Methods

testCoercion :: forall (a :: k) (b :: k). IsUnion x y a -> IsUnion x y b -> Maybe (Coercion a b)

Eq (IsUnion x y z)

Defined in Newtype.Union

Methods

(==) :: IsUnion x y z -> IsUnion x y z -> Bool

(/=) :: IsUnion x y z -> IsUnion x y z -> Bool

Ord (IsUnion x y z)

Defined in Newtype.Union

Methods

compare :: IsUnion x y z -> IsUnion x y z -> Ordering

(<) :: IsUnion x y z -> IsUnion x y z -> Bool

(<=) :: IsUnion x y z -> IsUnion x y z -> Bool

(>) :: IsUnion x y z -> IsUnion x y z -> Bool

(>=) :: IsUnion x y z -> IsUnion x y z -> Bool

max :: IsUnion x y z -> IsUnion x y z -> IsUnion x y z

min :: IsUnion x y z -> IsUnion x y z -> IsUnion x y z

withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r

For a pair of Related types x and y, make some (existentially quantified) type xy where xy is a union type of x, y.

unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'

Two union types z,z' of the same pair of types x,y may be different, but they are equivalent in terms of coercibility.

greater :: Sub x y -> IsUnion x y y

When Sub x y, y itself is a union type of x, y.

idemp :: IsUnion x x x

Union is idempotent.

Note: combining idemp and unique, IsUnion x x z -> Coercion x z holds.

commutative :: IsUnion x y z -> IsUnion y x z

Union is commutative.

Note: combining commutative and unique, IsUnion x y xy -> IsUnion y x yx -> Coercion xy yx holds.

associative :: IsUnion x y xy -> IsUnion xy z xyz -> IsUnion y z yz -> IsUnion x yz xyz

Union is associative.

Note: combining associative and unique, the following holds.

   IsUnion x y xy -> IsUnion xy z xy'z
-> IsUnion y z yz -> IsUnion x yz x'yz
-> Coercion xy'z x'yz