Data.Type.Coercion.Related

Related type to witness that two types a and b shares the same runtime representation, but nothing about whether a can be safely coerced to or from b.

Unlike Coercion or Sub, having a value of Related a b does not allow to touch values of a or b.

This module is used alonside Newtype.Union and Newtype.Intersection to define union and intersection types of two Related types.

Documentation

data Related (a :: k) (b :: k)

Related a b witnesses a and b shares the same runtime representation, but nothing about whether a can be safely coerced to or from b.

You can make Related witnesses by using combinators in this module, or the methods of the Category Related instance: id and (.).

Instances

Category (Related :: k -> k -> Type)

Defined in Data.Type.Coercion.Related.Internal

Methods

id :: forall (a :: k0). Related a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). Related b c -> Related a b -> Related a c

Coercible a b => Bounded (Related a b)

Defined in Data.Type.Coercion.Related.Internal

Methods

minBound :: Related a b

maxBound :: Related a b

Coercible a b => Enum (Related a b)

Defined in Data.Type.Coercion.Related.Internal

Methods

succ :: Related a b -> Related a b

pred :: Related a b -> Related a b

toEnum :: Int -> Related a b

fromEnum :: Related a b -> Int

enumFrom :: Related a b -> [Related a b]

enumFromThen :: Related a b -> Related a b -> [Related a b]

enumFromTo :: Related a b -> Related a b -> [Related a b]

enumFromThenTo :: Related a b -> Related a b -> Related a b -> [Related a b]

Coercible a b => Read (Related a b)

Defined in Data.Type.Coercion.Related.Internal

Methods

readsPrec :: Int -> ReadS (Related a b)

readList :: ReadS [Related a b]

readPrec :: ReadPrec (Related a b)

readListPrec :: ReadPrec [Related a b]

Show (Related a b)

Defined in Data.Type.Coercion.Related.Internal

Methods

showsPrec :: Int -> Related a b -> ShowS

show :: Related a b -> String

showList :: [Related a b] -> ShowS

Eq (Related a b)

Defined in Data.Type.Coercion.Related.Internal

Methods

(==) :: Related a b -> Related a b -> Bool

(/=) :: Related a b -> Related a b -> Bool

Ord (Related a b)

Defined in Data.Type.Coercion.Related.Internal

Methods

compare :: Related a b -> Related a b -> Ordering

(<) :: Related a b -> Related a b -> Bool

(<=) :: Related a b -> Related a b -> Bool

(>) :: Related a b -> Related a b -> Bool

(>=) :: Related a b -> Related a b -> Bool

max :: Related a b -> Related a b -> Related a b

min :: Related a b -> Related a b -> Related a b

related :: Coercible a b => Related a b

Coercible a b implies Related a b.

subIsRelated :: Sub (Sub a b) (Related a b)

Sub a b implies Related a b.

coercionIsRelated :: Sub (Coercion a b) (Related a b)

Coercion a b implies Sub a b, which implies Related a b.

symRelated :: Related a b -> Related b a

Related is a symmetric relation.

undirected :: Sub a b -> (Coercible a b => Related x y) -> Related x y

A direct consequence of informRelation and subIsRelated.

informRelation :: Related a b -> (Coercible a b => Related x y) -> Related x y

Given Related a b, you can assume Coercible a b for the purpose of proving another Related relation.