Data.Type.Coercion.Sub

Documentation

Sub a b witnesses a zero-cost conversion a -> b.

Sub is a newtype wrapper around Coercion, but made opaque to hide the ability to coerce into other direction.

This is convenient for newtype wrappers which give additional guarantees.

As an example, think about the following code:

-- | A pair @(x::a, y::a)@, but guaranteed @x <= y@
newtype Range a = MkRange (a,a)

getRange :: Range a -> (a,a)
getRange = coerce
mkRange :: Ord a => a -> a -> Range a
mkRange x y = if x <= y then MkRange (x,y) else MkRange (y,x)

If you want to provide this type from a library you maintain, you would want to keep Range abstract from outside of the module.

An user may want to convert [Range a] to [(a,a)] without actually traversing the list. This is possible if the user have access to the internals, or you export a Coercion (Range a) (a,a) value. But doing so breaks the guarantee, because it also allows to use Coercible in the other direction, as in coerce (10,5) :: Range Int.

By exporting only Sub (Range a) (a,a) value from your module, this user can get Sub [Range a] [(a,a)] using mapR, without being able to make an invalid value.

data Sub (a :: k) (b :: k)

Instances

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

Defined in Data.Type.Coercion.Sub.Internal

Methods

id :: Sub a a

(.) :: Sub b c -> Sub a b -> Sub a c

Eq (Sub a b)

Defined in Data.Type.Coercion.Sub.Internal

Methods

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

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

Ord (Sub a b)

Defined in Data.Type.Coercion.Sub.Internal

Methods

compare :: Sub a b -> Sub a b -> Ordering

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

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

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

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

max :: Sub a b -> Sub a b -> Sub a b

min :: Sub a b -> Sub a b -> Sub a b

Show (Sub a b)

Defined in Data.Type.Coercion.Sub.Internal

Methods

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

show :: Sub a b -> String

showList :: [Sub a b] -> ShowS

sub :: Coercible a b => Sub a b

Make a witness for type-safe casting which respects direction.

toSub :: Coercion a b -> Sub a b

upcastWith :: Sub a b -> a -> b

Type-safe cast

equiv :: Sub a b -> Sub b a -> Coercion a b

Sub relation in both direction means there is Coercion relation.

gequiv :: Sub a b -> Sub b a -> (Coercible a b => r) -> r

Generalized equiv

coercionIsSub :: Sub (Coercion a b) (Sub a b)

All Coercion can be seen as Sub

mapR :: (forall x x'. Coercible x x' => Coercible (t x) (t x'), Functor t) => Sub a b -> Sub (t a) (t b)

Extend subtype relation covariantly.

contramapR :: (forall x x'. Coercible x x' => Coercible (t x) (t x'), Contravariant t) => Sub a b -> Sub (t b) (t a)

Extend subtype relation contravariantly

bimapR :: (forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (t x y) (t x' y'), Bifunctor t) => Sub a a' -> Sub b b' -> Sub (t a b) (t a' b')

dimapR :: (forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (t x y) (t x' y'), Profunctor t) => Sub a a' -> Sub b b' -> Sub (t a' b) (t a b')