{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Attenuation.Internal
( Attenuation(..), Attenuable(..)
, Variance, Representational, Representational0, Representational1
, refl, trans, co, fstco, sndco, domain, codomain, rep, rep0
, withAttenuation
) where
import Prelude hiding ((.))
import Control.Category (Category(..))
import Data.Bifunctor (Bifunctor)
import Data.Coerce (Coercible)
import Data.Kind (Constraint, Type)
import Data.Type.Coercion (Coercion(..), sym)
import qualified Data.Type.Coercion as Coercion
#if MIN_VERSION_constraints(0, 11, 0)
import Data.Constraint (Dict(..), HasDict(..))
#endif
type Representational f =
(forall a b. Coercible a b => Coercible (f a) (f b) :: Constraint)
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)
type Variance s t a b = Attenuation a b -> Attenuation s t
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
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
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 k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
/= :: Attenuation a b -> Attenuation a b -> Bool
$c/= :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
== :: Attenuation a b -> Attenuation a b -> Bool
$c== :: forall k (a :: k) (b :: k).
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 k (a :: k) (b :: k). Eq (Attenuation a b)
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Ordering
forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Attenuation a b
min :: Attenuation a b -> Attenuation a b -> Attenuation a b
$cmin :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Attenuation a b
max :: Attenuation a b -> Attenuation a b -> Attenuation a b
$cmax :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Attenuation a b
>= :: Attenuation a b -> Attenuation a b -> Bool
$c>= :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
> :: Attenuation a b -> Attenuation a b -> Bool
$c> :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
<= :: Attenuation a b -> Attenuation a b -> Bool
$c<= :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
< :: Attenuation a b -> Attenuation a b -> Bool
$c< :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Bool
compare :: Attenuation a b -> Attenuation a b -> Ordering
$ccompare :: forall k (a :: k) (b :: k).
Attenuation a b -> Attenuation a b -> Ordering
$cp1Ord :: forall k (a :: k) (b :: k). 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 k (a :: k) (b :: k). Int -> Attenuation a b -> ShowS
forall k (a :: k) (b :: k). [Attenuation a b] -> ShowS
forall k (a :: k) (b :: k). Attenuation a b -> String
showList :: [Attenuation a b] -> ShowS
$cshowList :: forall k (a :: k) (b :: k). [Attenuation a b] -> ShowS
show :: Attenuation a b -> String
$cshow :: forall k (a :: k) (b :: k). Attenuation a b -> String
showsPrec :: Int -> Attenuation a b -> ShowS
$cshowsPrec :: forall k (a :: k) (b :: k). Int -> Attenuation a b -> ShowS
Show)
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 k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f a) (f b)
forall k k (f :: k -> k) (a :: k) (b :: k).
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 k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f a x) (f b x)
forall k k k (f :: k -> k -> k) (a :: k) (b :: k) (x :: k).
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 k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (f x a) (f x b)
forall k k (f :: k -> k) (a :: k) (b :: k).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
domain :: Variance (b -> x) (a -> x) a b
domain :: Variance (b -> x) (a -> x) a b
domain (Attenuation Coercion a b
c) = Coercion (b -> x) (a -> x) -> Attenuation (b -> x) (a -> x)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion (a -> x) (b -> x) -> Coercion (b -> x) (a -> x)
forall k (a :: k) (b :: k). Coercion a b -> Coercion b a
sym (Coercion (a -> x) (b -> x) -> Coercion (b -> x) (a -> x))
-> Coercion (a -> x) (b -> x) -> Coercion (b -> x) (a -> x)
forall a b. (a -> b) -> a -> b
$ Coercion a b -> Coercion (a -> x) (b -> x)
forall k k k (f :: k -> k -> k) (a :: k) (b :: k) (x :: k).
Representational0 f =>
Coercion a b -> Coercion (f a x) (f b x)
rep0 Coercion a b
c)
codomain :: Variance (x -> a) (x -> b) a b
codomain :: Variance (x -> a) (x -> b) a b
codomain (Attenuation Coercion a b
c) = Coercion (x -> a) (x -> b) -> Attenuation (x -> a) (x -> b)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation (Coercion a b -> Coercion (x -> a) (x -> b)
forall k k (f :: k -> k) (a :: k) (b :: k).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r
withAttenuation :: Attenuation a b -> (Attenuable a b => r) -> r
withAttenuation (Attenuation Coercion a b
Coercion) Attenuable a b => r
r = r
Attenuable a b => r
r
instance {-# INCOHERENT #-} Coercible a b => Attenuable a b
instance {-# INCOHERENT #-} Attenuable (a :: Type) a
#if MIN_VERSION_constraints(0, 11, 0)
instance HasDict (Attenuable a b) (Attenuation a b) where
evidence :: Attenuation a b -> Dict (Attenuable a b)
evidence = (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` Attenuable a b => Dict (Attenuable a b)
forall (a :: Constraint). a => Dict a
Dict)
#endif
instance {-# INCOHERENT #-} (Functor f, Representational f, Attenuable x y)
=> Attenuable (f x) (f y) where
attenuation :: Attenuation (f x) (f y)
attenuation = Variance (f x) (f y) x y
forall (f :: * -> *) a b.
(Functor f, Representational f) =>
Variance (f a) (f b) a b
co Attenuation x y
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
instance {-# INCOHERENT #-}
( Bifunctor f, Representational0 f, Representational1 f
, Attenuable a c
, Attenuable b d
)
=> Attenuable (f a b) (f c d) where
attenuation :: Attenuation (f a b) (f c d)
attenuation = Variance (f a d) (f c d) a c
forall (f :: * -> * -> *) a x b.
(Bifunctor f, Representational0 f) =>
Variance (f a x) (f b x) a b
fstco Attenuation a c
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (f a d) (f c d)
-> Attenuation (f a b) (f a d) -> Attenuation (f a b) (f c d)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (f a b) (f a d) b d
forall (f :: * -> * -> *) x a b.
(Bifunctor f, Representational1 f) =>
Variance (f x a) (f x b) a b
sndco Attenuation b d
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
instance (Attenuable c a, Attenuable b d)
=> Attenuable (a -> b) (c -> d) where
attenuation :: Attenuation (a -> b) (c -> d)
attenuation = Variance (a -> d) (c -> d) c a
forall b x a. Variance (b -> x) (a -> x) a b
domain Attenuation c a
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (a -> d) (c -> d)
-> Attenuation (a -> b) (a -> d) -> Attenuation (a -> b) (c -> d)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a -> b) (a -> d) b d
forall x a b. Variance (x -> a) (x -> b) a b
codomain Attenuation b d
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
instance (Attenuable a a', Attenuable b b')
=> Attenuable (a, b) (a', b') where
attenuation :: Attenuation (a, b) (a', b')
attenuation = Variance (a, b') (a', b') a a'
forall (f :: * -> * -> *) a x b.
(Bifunctor f, Representational0 f) =>
Variance (f a x) (f b x) a b
fstco Attenuation a a'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (a, b') (a', b')
-> Attenuation (a, b) (a, b') -> Attenuation (a, b) (a', b')
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a, b) (a, b') b b'
forall (f :: * -> * -> *) x a b.
(Bifunctor f, Representational1 f) =>
Variance (f x a) (f x b) a b
sndco Attenuation b b'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
instance (Attenuable a a', Attenuable b b', Attenuable c c')
=> Attenuable (a, b, c) (a', b', c') where
attenuation :: Attenuation (a, b, c) (a', b', c')
attenuation = Attenuation (a, b', c') (a', b', c')
fst3 Attenuation (a, b', c') (a', b', c')
-> Attenuation (a, b, c) (a, b', c')
-> Attenuation (a, b, c) (a', b', c')
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a, b, c') (a, b', c') b b'
forall (f :: * -> * -> *) a x b.
(Bifunctor f, Representational0 f) =>
Variance (f a x) (f b x) a b
fstco Attenuation b b'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation Attenuation (a, b, c') (a, b', c')
-> Attenuation (a, b, c) (a, b, c')
-> Attenuation (a, b, c) (a, b', c')
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Variance (a, b, c) (a, b, c') c c'
forall (f :: * -> * -> *) x a b.
(Bifunctor f, Representational1 f) =>
Variance (f x a) (f x b) a b
sndco Attenuation c c'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
where
fst3 :: Attenuation (a, b', c') (a', b', c')
fst3 :: Attenuation (a, b', c') (a', b', c')
fst3 = case Attenuable a a' => Attenuation a a'
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation @a @a' of Attenuation Coercion a a'
Coercion -> Attenuation (a, b', c') (a', b', c')
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
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 k (a :: k) (b :: k). 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)
refl :: Attenuation a a
refl :: Attenuation a a
refl = Coercion a a -> Attenuation a a
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
instance Category Attenuation where
id :: Attenuation a a
id = Attenuation a a
forall k (a :: k). Attenuation a a
refl
. :: 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 k (a :: k) (b :: k) (c :: k).
Attenuation a b -> Attenuation b c -> Attenuation a c
trans
class Attenuable a b where
attenuation :: Attenuation a b
default attenuation :: Coercible a b => Attenuation a b
attenuation = Coercion a b -> Attenuation a b
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion