{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Attenuation
(
Attenuation, attenuate, coercible
, trans, repr, coer
, Representational, Representational0, Representational1, Variance
, co, contra
, fstco, sndco
, lcontra, rco
, attVoid, attAny
) where
import Control.Category (Category(..))
import Data.Bifunctor (Bifunctor)
import Data.Coerce (Coercible, coerce)
import Data.Functor.Contravariant (Contravariant)
import Data.Kind (Constraint)
import Data.Profunctor (Profunctor)
import Data.Type.Coercion (Coercion(..), sym)
import qualified Data.Type.Coercion as Coercion
import Data.Type.Equality ((:~:)(..))
import Data.Void (Void)
import GHC.Exts (Any)
#if MIN_VERSION_base(4,15,0)
import Unsafe.Coerce (unsafeEqualityProof, UnsafeEquality(..))
#else
import Unsafe.Coerce (unsafeCoerce)
#endif
newtype Attenuation a b = Attenuation (Coercion a b)
deriving (Attenuation a b -> Attenuation a b -> Bool
(Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> Eq (Attenuation a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. Attenuation a b -> Attenuation a b -> Bool
/= :: Attenuation a b -> Attenuation a b -> Bool
$c/= :: forall a b. Attenuation a b -> Attenuation a b -> Bool
== :: Attenuation a b -> Attenuation a b -> Bool
$c== :: forall a b. Attenuation a b -> Attenuation a b -> Bool
Eq, Eq (Attenuation a b)
Eq (Attenuation a b)
-> (Attenuation a b -> Attenuation a b -> Ordering)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Bool)
-> (Attenuation a b -> Attenuation a b -> Attenuation a b)
-> (Attenuation a b -> Attenuation a b -> Attenuation a b)
-> Ord (Attenuation a b)
Attenuation a b -> Attenuation a b -> Bool
Attenuation a b -> Attenuation a b -> Ordering
Attenuation a b -> Attenuation a b -> Attenuation a b
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a b. Eq (Attenuation a b)
forall a b. Attenuation a b -> Attenuation a b -> Bool
forall a b. Attenuation a b -> Attenuation a b -> Ordering
forall a b. Attenuation a b -> Attenuation a b -> Attenuation a b
min :: Attenuation a b -> Attenuation a b -> Attenuation a b
$cmin :: forall a b. Attenuation a b -> Attenuation a b -> Attenuation a b
max :: Attenuation a b -> Attenuation a b -> Attenuation a b
$cmax :: forall a b. Attenuation a b -> Attenuation a b -> Attenuation a b
>= :: Attenuation a b -> Attenuation a b -> Bool
$c>= :: forall a b. Attenuation a b -> Attenuation a b -> Bool
> :: Attenuation a b -> Attenuation a b -> Bool
$c> :: forall a b. Attenuation a b -> Attenuation a b -> Bool
<= :: Attenuation a b -> Attenuation a b -> Bool
$c<= :: forall a b. Attenuation a b -> Attenuation a b -> Bool
< :: Attenuation a b -> Attenuation a b -> Bool
$c< :: forall a b. Attenuation a b -> Attenuation a b -> Bool
compare :: Attenuation a b -> Attenuation a b -> Ordering
$ccompare :: forall a b. Attenuation a b -> Attenuation a b -> Ordering
$cp1Ord :: forall a b. Eq (Attenuation a b)
Ord, Int -> Attenuation a b -> ShowS
[Attenuation a b] -> ShowS
Attenuation a b -> String
(Int -> Attenuation a b -> ShowS)
-> (Attenuation a b -> String)
-> ([Attenuation a b] -> ShowS)
-> Show (Attenuation a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. Int -> Attenuation a b -> ShowS
forall a b. [Attenuation a b] -> ShowS
forall a b. Attenuation a b -> String
showList :: [Attenuation a b] -> ShowS
$cshowList :: forall a b. [Attenuation a b] -> ShowS
show :: Attenuation a b -> String
$cshow :: forall a b. Attenuation a b -> String
showsPrec :: Int -> Attenuation a b -> ShowS
$cshowsPrec :: forall a b. Int -> Attenuation a b -> ShowS
Show)
instance Category Attenuation where
id :: Attenuation a a
id = Attenuation a a
forall a b. Coercible a b => Attenuation a b
coercible
. :: Attenuation b c -> Attenuation a b -> Attenuation a c
(.) = (Attenuation a b -> Attenuation b c -> Attenuation a c)
-> Attenuation b c -> Attenuation a b -> Attenuation a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Attenuation a b -> Attenuation b c -> Attenuation a c
forall a b c. Attenuation a b -> Attenuation b c -> Attenuation a c
trans
attenuate :: Attenuation a b -> a -> b
attenuate :: Attenuation a b -> a -> b
attenuate (Attenuation Coercion a b
Coercion) = a -> b
coerce
coercible :: Coercible a b => Attenuation a b
coercible :: Attenuation a b
coercible = Coercion a b -> Attenuation a b
forall a b. Coercion a b -> Attenuation a b
Attenuation Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
trans :: Attenuation a b -> Attenuation b c -> Attenuation a c
trans (Attenuation Coercion a b
coAB) (Attenuation Coercion b c
coBC) =
Coercion a c -> Attenuation a c
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion b c -> Coercion a c
forall k (a :: k) (b :: k) (c :: k).
Coercion a b -> Coercion b c -> Coercion a c
Coercion.trans Coercion a b
coAB Coercion b c
coBC)
repr :: (a :~: b) -> Attenuation a b
repr :: (a :~: b) -> Attenuation a b
repr a :~: b
Refl = Coercion a b -> Attenuation a b
forall a b. Coercion a b -> Attenuation a b
Attenuation Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
coer :: Coercion a b -> Attenuation a b
coer :: Coercion a b -> Attenuation a b
coer = Coercion a b -> Attenuation a b
forall a b. Coercion a b -> Attenuation a b
Attenuation
type Variance s t a b = Attenuation a b -> Attenuation s t
type Representational f =
(forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint)
rep :: Representational f => Coercion a b -> Coercion (f a) (f b)
rep :: Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
Coercion = Coercion (f a) (f b)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
type Representational1 f =
(forall a b x. Coercible a b => Coercible (f x a) (f x b) :: Constraint)
type Representational0 f =
(forall a b x. Coercible a b => Coercible (f a x) (f b x) :: Constraint)
rep0 :: Representational0 f => Coercion a b -> Coercion (f a x) (f b x)
rep0 :: Coercion a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
Coercion = Coercion (f a x) (f b x)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
co :: (Functor f, Representational f) => Variance (f a) (f b) a b
co :: Variance (f a) (f b) a b
co (Attenuation Coercion a b
c) = Coercion (f a) (f b) -> Attenuation (f a) (f b)
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f a) (f b)
forall (f :: * -> *) a b.
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
contra :: (Contravariant f, Representational f) => Variance (f b) (f a) a b
contra :: Variance (f b) (f a) a b
contra (Attenuation Coercion a b
c) = Coercion (f b) (f a) -> Attenuation (f b) (f a)
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion (f a) (f b) -> Coercion (f b) (f a)
forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (Coercion (f a) (f b) -> Coercion (f b) (f a))
-> Coercion (f a) (f b) -> Coercion (f b) (f a)
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Coercion (f a) (f b)
forall (f :: * -> *) a b.
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
fstco :: (Bifunctor f, Representational0 f) => Variance (f a x) (f b x) a b
fstco :: Variance (f a x) (f b x) a b
fstco (Attenuation Coercion a b
c) = Coercion (f a x) (f b x) -> Attenuation (f a x) (f b x)
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f a x) (f b x)
forall (f :: * -> * -> *) a b x.
Representational0 f =>
Coercion a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
c)
sndco :: (Bifunctor f, Representational1 f) => Variance (f x a) (f x b) a b
sndco :: Variance (f x a) (f x b) a b
sndco (Attenuation Coercion a b
c) = Coercion (f x a) (f x b) -> Attenuation (f x a) (f x b)
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f x a) (f x b)
forall (f :: * -> *) a b.
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
lcontra :: (Profunctor p, Representational0 p) => Variance (p b x) (p a x) a b
lcontra :: Variance (p b x) (p a x) a b
lcontra (Attenuation Coercion a b
c) = Coercion (p b x) (p a x) -> Attenuation (p b x) (p a x)
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion (p a x) (p b x) -> Coercion (p b x) (p a x)
forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (Coercion (p a x) (p b x) -> Coercion (p b x) (p a x))
-> Coercion (p a x) (p b x) -> Coercion (p b x) (p a x)
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Coercion (p a x) (p b x)
forall (f :: * -> * -> *) a b x.
Representational0 f =>
Coercion a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
c)
rco :: (Profunctor p, Representational1 p) => Variance (p x a) (p x b) a b
rco :: Variance (p x a) (p x b) a b
rco (Attenuation Coercion a b
c) = Coercion (p x a) (p x b) -> Attenuation (p x a) (p x b)
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (p x a) (p x b)
forall (f :: * -> *) a b.
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
attVoid :: forall a. Attenuation Void a
attVoid :: Attenuation Void a
attVoid = Coercion Void a -> Attenuation Void a
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion Void a -> Attenuation Void a)
-> Coercion Void a -> Attenuation Void a
forall a b. (a -> b) -> a -> b
$
#if MIN_VERSION_base(4,15,0)
case unsafeEqualityProof :: UnsafeEquality a Void of UnsafeRefl -> Coercion
#else
(Coercion a a -> Coercion Void a
forall a b. a -> b
unsafeCoerce (Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion :: Coercion a a) :: Coercion Void a)
#endif
attAny :: forall a. Attenuation a Any
attAny :: Attenuation a Any
attAny = Coercion a Any -> Attenuation a Any
forall a b. Coercion a b -> Attenuation a b
Attenuation (Coercion a Any -> Attenuation a Any)
-> Coercion a Any -> Attenuation a Any
forall a b. (a -> b) -> a -> b
$
#if MIN_VERSION_base(4,15,0)
case unsafeEqualityProof :: UnsafeEquality a Any of UnsafeRefl -> Coercion
#else
(Coercion a a -> Coercion a Any
forall a b. a -> b
unsafeCoerce (Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion :: Coercion a a) :: Coercion a Any)
#endif