Newtype.Intersection

Documentation

module Data.Type.Coercion.Related

data IsIntersection x y z

IsIntersection x y z witnesses the fact:

• All x, y, z share the same runtime representation

• z is an intersection type of x and y. In other words, the following three holds:

  • Sub z x

  • Sub z y

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

Constructors

IsIntersection

Fields

• proj1 :: !(Sub z x)
• proj2 :: !(Sub z y)
• conjunct :: forall s. Sub s x -> Sub s y -> Sub s z

Instances

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

Defined in Newtype.Intersection

Methods

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

Eq (IsIntersection x y z)

Defined in Newtype.Intersection

Methods

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

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

Ord (IsIntersection x y z)

Defined in Newtype.Intersection

Methods

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

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

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

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

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

max :: IsIntersection x y z -> IsIntersection x y z -> IsIntersection x y z

min :: IsIntersection x y z -> IsIntersection x y z -> IsIntersection x y z

withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r

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

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

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

lesser :: Sub x y -> IsIntersection x y x

When Sub x y, x itself is an intersection type of x, y.

idemp :: IsIntersection x x x

Intersection is idempotent.

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

commutative :: IsIntersection x y z -> IsIntersection y x z

Intersection is commutative.

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

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

Intersection is associative.

Note: combining associative and unique, the following holds.

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