Safe Haskell	Safe-Inferred
Language	Haskell2010

Newtype.Union

Synopsis

module Data.Type.Coercion.Related
data IsUnion x y z = IsUnion {
- inl :: !(Sub x z)
- inr :: !(Sub y z)
- elim :: forall r. Sub x r -> Sub y r -> Sub z r
}
withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r
unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'
greater :: Sub x y -> IsUnion x y y
idemp :: IsUnion x x x
commutative :: IsUnion x y z -> IsUnion y x z
associative :: IsUnion x y xy -> IsUnion xy z xyz -> IsUnion y z yz -> IsUnion x yz xyz

Documentation

IsUnion x y z witnesses the fact:

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 details

TestCoercion (IsUnion x y :: Type -> Type) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

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

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

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

Union is idempotent.

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

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 Source #

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