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

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 -> Coercible x z holds.

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

Intersection is commutative.

Note: combining commutative and unique, IsIntersection x x z -> Coercible x z holds.

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

Intersection is associative.