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.

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 -> Coercible 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 -> Coercible xy yx holds.

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

Union is associative.