{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeOperators #-}
module Data.Type.Attenuation.Profunctor
(
lcontra, rco, profunctoriality
) where
import Prelude hiding ((.))
import Control.Category ((.))
import Data.Constraint ((:-)(Sub), Dict(..))
import Data.Profunctor (Profunctor)
import Data.Type.Attenuation
( Attenuation, Attenuable
, Variance, Representational0, Representational1
, coer, attenuation, withAttenuation
)
import Data.Type.Attenuation.Internal (Attenuation(..), rep0, rep)
import Data.Type.Coercion (sym)
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 k (a :: k) (b :: k). Coercion a b -> Attenuation a b
coer (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 k1 k2 k3 (f :: k1 -> k2 -> k3) (a :: k1) (b :: k1)
(x :: k2).
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 k (a :: k) (b :: k). Coercion a b -> Attenuation a b
coer (Coercion a b -> Coercion (p x a) (p x b)
forall k1 k2 (f :: k1 -> k2) (a :: k1) (b :: k1).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
toDict :: Attenuation a b -> Dict (Attenuable a b)
toDict :: Attenuation a b -> Dict (Attenuable a b)
toDict Attenuation a b
att = Attenuation a b
-> (Attenuable a b => Dict (Attenuable a b))
-> Dict (Attenuable a b)
forall k (a :: k) (b :: k) r.
Attenuation a b -> (Attenuable a b => r) -> r
withAttenuation Attenuation a b
att Attenuable a b => Dict (Attenuable a b)
forall (a :: Constraint). a => Dict a
Dict
profunctoriality
:: forall p a b c d
. (Representational0 p, Representational1 p, Profunctor p)
=> (Attenuable a c, Attenuable b d) :- Attenuable (p c b) (p a d)
profunctoriality :: (Attenuable a c, Attenuable b d) :- Attenuable (p c b) (p a d)
profunctoriality = ((Attenuable a c, Attenuable b d) =>
Dict (Attenuable (p c b) (p a d)))
-> (Attenuable a c, Attenuable b d) :- Attenuable (p c b) (p a d)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Attenuation (p c b) (p a d) -> Dict (Attenuable (p c b) (p a d))
forall a b. Attenuation a b -> Dict (Attenuable a b)
toDict (Variance (p a b) (p a d) b d
forall (p :: * -> * -> *) x a b.
(Profunctor p, Representational1 p) =>
Variance (p x a) (p x b) a b
rco Attenuation b d
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (p a b) (p a d)
-> Attenuation (p c b) (p a b) -> Attenuation (p c b) (p a d)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (p c b) (p a b) a c
forall (p :: * -> * -> *) b x a.
(Profunctor p, Representational0 p) =>
Variance (p b x) (p a x) a b
lcontra Attenuation a c
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation))