Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Type.Coercion.Sub

Description

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

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.

A 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.

Synopsis

data Sub (a :: k) (b :: k)
sub :: Coercible a b => Sub a b
toSub :: Coercion a b -> Sub a b
upcastWith :: Sub a b -> a -> b
equiv :: Sub a b -> Sub b a -> Coercion a b
gequiv :: Sub a b -> Sub b a -> (Coercible a b => r) -> r
coercionIsSub :: Sub (Coercion a b) (Sub a b)
instantiate :: forall j k (f :: j -> k) (g :: j -> k) (a :: j). Sub f g -> Sub (f a) (g a)
mapR :: (forall x x'. Coercible x x' => Coercible (t x) (t x'), Functor t) => Sub a b -> Sub (t a) (t b)
contramapR :: (forall x x'. Coercible x x' => Coercible (t x) (t x'), Contravariant t) => Sub a b -> Sub (t b) (t a)
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')
prodR :: Sub a a' -> Sub b b' -> Sub (a, b) (a', b')
prod3R :: Sub a a' -> Sub b b' -> Sub c c' -> Sub (a, b, c) (a', b', c')
sumR :: Sub a a' -> Sub b b' -> Sub (Either a b) (Either 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')
arrR :: Sub a a' -> Sub b b' -> Sub (a' -> b) (a -> b')

Documentation

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

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.

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

Instances

Instances details

Category (Sub :: k -> k -> Type) Source #
Instance details Defined in Data.Type.Coercion.Sub.Internal Methods id :: forall (a :: k0). Sub a a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). Sub b c -> Sub a b -> Sub a c #
Coercible a b => Bounded (Sub a b) Source #
Instance details Defined in Data.Type.Coercion.Sub.Internal Methods minBound :: Sub a b # maxBound :: Sub a b #
Coercible a b => Enum (Sub a b) Source #
Instance details Defined in Data.Type.Coercion.Sub.Internal Methods succ :: Sub a b -> Sub a b # pred :: Sub a b -> Sub a b # toEnum :: Int -> Sub a b # fromEnum :: Sub a b -> Int # enumFrom :: Sub a b -> [Sub a b] # enumFromThen :: Sub a b -> Sub a b -> [Sub a b] # enumFromTo :: Sub a b -> Sub a b -> [Sub a b] # enumFromThenTo :: Sub a b -> Sub a b -> Sub a b -> [Sub a b] #
Coercible a b => Read (Sub a b) Source #
Instance details Defined in Data.Type.Coercion.Sub.Internal Methods readsPrec :: Int -> ReadS (Sub a b) # readList :: ReadS [Sub a b] # readPrec :: ReadPrec (Sub a b) # readListPrec :: ReadPrec [Sub a b] #
Show (Sub a b) Source #
Instance details Defined in Data.Type.Coercion.Sub.Internal Methods showsPrec :: Int -> Sub a b -> ShowS # show :: Sub a b -> String # showList :: [Sub a b] -> ShowS #
Eq (Sub a b) Source #
Instance details 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) Source #
Instance details 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 #

sub :: Coercible a b => Sub a b Source #

Make a directed witness of coerce :: a -> b.

toSub :: Coercion a b -> Sub a b Source #

Make a directed witness of coerce :: a -> b, from a Coercion value.

upcastWith :: Sub a b -> a -> b Source #

Type-safe cast

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

Sub relation in both direction means there is Coercion relation.

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

Generalized equiv

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

All Coercion can be seen as Sub

instantiate :: forall j k (f :: j -> k) (g :: j -> k) (a :: j). Sub f g -> Sub (f a) (g a) Source #

For a Sub relation between type constructors f and g, create an instance of subtype relation Sub (f a) (g a) for any type parameter a.

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

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) Source #

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') Source #

Extend subtype relation over a Bifunctor.

prodR :: Sub a a' -> Sub b b' -> Sub (a, b) (a', b') infixr 3 Source #

bimapR specialized for the pair type '(a,b)'

prod3R :: Sub a a' -> Sub b b' -> Sub c c' -> Sub (a, b, c) (a', b', c') Source #

Extend subtype relation over the 3-tuple types '(a,b,c)'

sumR :: Sub a a' -> Sub b b' -> Sub (Either a b) (Either a' b') infixr 2 Source #

bimapR specialized for Either

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') Source #

Extend subtype relation over a Profunctor.

arrR :: Sub a a' -> Sub b b' -> Sub (a' -> b) (a -> b') infixr 1 Source #

dimapR specialized for functions (->)