Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- module Data.Type.Coercion.Related
- data IsIntersection x y z = IsIntersection {}
- withIntersection :: Related x y -> (forall xy. IsIntersection x y xy -> r) -> r
- unique :: IsIntersection x y z -> IsIntersection x y z' -> Coercion z z'
- lesser :: Sub x y -> IsIntersection x y x
- idemp :: IsIntersection x x x
- commutative :: IsIntersection x y z -> IsIntersection y x z
- associative :: IsIntersection x y xy -> IsIntersection xy z xyz -> IsIntersection y z yz -> IsIntersection x yz xyz
Documentation
module Data.Type.Coercion.Related
data IsIntersection x y z Source #
IsIntersection x y z
witnesses the fact:
- All
x, y, z
share the same runtime representation z
is an intersection type ofx
andy
. In other words, the following three holds:Sub
z xSub z y
- For any type
s
satisfying both of(Sub s x, Sub s y)
,Sub s z
.
Instances
TestCoercion (IsIntersection x y :: Type -> Type) Source # | |
Defined in Newtype.Intersection testCoercion :: forall (a :: k) (b :: k). IsIntersection x y a -> IsIntersection x y b -> Maybe (Coercion a b) # | |
Eq (IsIntersection x y z) Source # | |
Defined in Newtype.Intersection (==) :: IsIntersection x y z -> IsIntersection x y z -> Bool # (/=) :: IsIntersection x y z -> IsIntersection x y z -> Bool # | |
Ord (IsIntersection x y z) Source # | |
Defined in Newtype.Intersection 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 Source #
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' Source #
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 Source #
When Sub x y
, x
itself is an intersection type of x, y
.
idemp :: IsIntersection x x x Source #
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 Source #
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 Source #
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