{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
module Data.Type.Coercion.Sub(
Sub(),
sub, toSub, upcastWith, equiv, gequiv,
coercionIsSub,
instantiate,
mapR, contramapR,
bimapR, prodR, prod3R, sumR, dimapR, arrR
) where
import Data.Coerce
import Data.Type.Coercion
import Data.Bifunctor (Bifunctor)
import Data.Functor.Contravariant (Contravariant)
import Data.Profunctor (Profunctor)
import Data.Type.Coercion.Sub.Internal
sub :: Coercible a b => Sub a b
sub :: forall {k} (a :: k) (b :: k). Coercible a b => Sub a b
sub = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
toSub :: Coercion a b -> Sub a b
toSub :: forall k (a :: k) (b :: k). Coercion a b -> Sub a b
toSub = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub
upcastWith :: Sub a b -> a -> b
upcastWith :: forall a b. Sub a b -> a -> b
upcastWith (Sub Coercion a b
Coercion) = coerce :: forall a b. Coercible a b => a -> b
coerce
coercionIsSub :: Sub (Coercion a b) (Sub a b)
coercionIsSub :: forall {k} (a :: k) (b :: k). Sub (Coercion a b) (Sub a b)
coercionIsSub = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
equiv :: Sub a b -> Sub b a -> Coercion a b
equiv :: forall {k} (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv Sub a b
ab Sub b a
ba = forall {k} (a :: k) (b :: k) r.
Sub a b -> Sub b a -> (Coercible a b => r) -> r
gequiv Sub a b
ab Sub b a
ba forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
gequiv :: Sub a b -> Sub b a -> (Coercible a b => r) -> r
gequiv :: forall {k} (a :: k) (b :: k) r.
Sub a b -> Sub b a -> (Coercible a b => r) -> r
gequiv (Sub Coercion a b
Coercion) (Sub Coercion b a
Coercion) Coercible a b => r
k = Coercible a b => r
k
instantiate :: forall j k (f :: j -> k) (g :: j -> k) (a :: j).
Sub f g -> Sub (f a) (g a)
instantiate :: forall j k (f :: j -> k) (g :: j -> k) (a :: j).
Sub f g -> Sub (f a) (g a)
instantiate (Sub Coercion f g
Coercion) = forall {k} (a :: k) (b :: k). Coercible a b => Sub a b
sub
mapR :: ( forall x x'. Coercible x x' => Coercible (t x) (t x')
, Functor t)
=> Sub a b -> Sub (t a) (t b)
mapR :: forall (t :: * -> *) a b.
(forall x x'. Coercible x x' => Coercible (t x) (t x'),
Functor t) =>
Sub a b -> Sub (t a) (t b)
mapR (Sub Coercion a b
Coercion) = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
contramapR :: ( forall x x'. Coercible x x' => Coercible (t x) (t x')
, Contravariant t)
=> Sub a b -> Sub (t b) (t a)
contramapR :: forall (t :: * -> *) a b.
(forall x x'. Coercible x x' => Coercible (t x) (t x'),
Contravariant t) =>
Sub a b -> Sub (t b) (t a)
contramapR (Sub Coercion a b
Coercion) = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
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')
bimapR :: forall (t :: * -> * -> *) a a' b b'.
(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')
bimapR (Sub Coercion a a'
Coercion) (Sub Coercion b b'
Coercion) = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
prodR :: Sub a a' -> Sub b b' -> Sub (a,b) (a',b')
prodR :: forall a a' b b'. Sub a a' -> Sub b b' -> Sub (a, b) (a', b')
prodR = forall (t :: * -> * -> *) a a' b b'.
(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')
bimapR
infixr 3 `prodR`
sumR :: Sub a a' -> Sub b b' -> Sub (Either a b) (Either a' b')
sumR :: forall a a' b b'.
Sub a a' -> Sub b b' -> Sub (Either a b) (Either a' b')
sumR = forall (t :: * -> * -> *) a a' b b'.
(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')
bimapR
infixr 2 `sumR`
prod3R :: Sub a a' -> Sub b b' -> Sub c c' -> Sub (a,b,c) (a',b',c')
prod3R :: forall a a' b b' c c'.
Sub a a' -> Sub b b' -> Sub c c' -> Sub (a, b, c) (a', b', c')
prod3R (Sub Coercion a a'
Coercion) (Sub Coercion b b'
Coercion) (Sub Coercion c c'
Coercion) = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
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')
dimapR :: forall (t :: * -> * -> *) a a' b b'.
(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')
dimapR (Sub Coercion a a'
Coercion) (Sub Coercion b b'
Coercion) = forall k (a :: k) (b :: k). Coercion a b -> Sub a b
Sub forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
arrR :: Sub a a' -> Sub b b' -> Sub (a' -> b) (a -> b')
arrR :: forall a a' b b'. Sub a a' -> Sub b b' -> Sub (a' -> b) (a -> b')
arrR = forall (t :: * -> * -> *) a a' b b'.
(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')
dimapR
infixr 1 `arrR`