{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Attenuation
(
Attenuation, type (:⊆:), attenuateWith, coercible
, trans, repr, coer, iso, inst
, Representational, Representational0, Representational1, Variance
, co, contra
, fstco, sndco
, domain, codomain
, attVoid, attAny
, Attenuable(..), type (⊆), attenuate
, withAttenuation
, contravariance, transitivity
) where
import Prelude hiding ((.))
import Control.Category (Category(..))
import Data.Coerce (Coercible, coerce)
import Data.Functor.Contravariant (Contravariant(..))
import Data.Type.Coercion (Coercion(..), sym)
import Data.Type.Equality ((:~:)(..), gcastWith)
import Data.Void (Void)
import GHC.Exts (Any)
import Data.Constraint ((:-)(Sub), Dict(..))
#if MIN_VERSION_base(4,15,0)
import Unsafe.Coerce (unsafeEqualityProof, UnsafeEquality(..))
#else
import Unsafe.Coerce (unsafeCoerce)
#endif
import Data.Type.Attenuation.Internal
type (:⊆:) = Attenuation
attenuateWith :: Attenuation a b -> a -> b
attenuateWith :: Attenuation a b -> a -> b
attenuateWith (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 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
repr :: (a :~: b) -> Attenuation a b
repr :: (a :~: b) -> Attenuation a b
repr a :~: b
eq = (a :~: b) -> ((a ~ b) => Attenuation a b) -> Attenuation a b
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith a :~: b
eq (a ~ b) => Attenuation a b
forall k (a :: k). Attenuation a a
refl
coer :: Coercion a b -> Attenuation a b
coer :: Coercion a b -> Attenuation a b
coer = Coercion a b -> Attenuation a b
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation
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 k (a :: k) (b :: k). 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 k1 k2 (f :: k1 -> k2) (a :: k1) (b :: k1).
Representational f =>
Coercion a b -> Coercion (f a) (f b)
rep Coercion a b
c)
inst :: Attenuation f g -> Attenuation (f x) (g x)
inst :: Attenuation f g -> Attenuation (f x) (g x)
inst (Attenuation Coercion f g
Coercion) = Coercion (f x) (g x) -> Attenuation (f x) (g x)
forall k (a :: k) (b :: k). Coercion a b -> Attenuation a b
Attenuation Coercion (f x) (g x)
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
attVoid :: forall a. Attenuation Void a
attVoid :: Attenuation Void a
attVoid = Coercion Void a -> Attenuation Void a
forall k (a :: k) (b :: k). 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 k (a :: k) (b :: k). 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
type (⊆) = Attenuable
attenuate :: Attenuable a b => a -> b
attenuate :: a -> b
attenuate = Attenuation a b -> a -> b
forall a b. Attenuation a b -> a -> b
attenuateWith Attenuation a b
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation
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
contravariance
:: forall f a b
. (Representational f, Contravariant f)
=> Attenuable a b :- Attenuable (f b) (f a)
contravariance :: Attenuable a b :- Attenuable (f b) (f a)
contravariance = (Attenuable a b => Dict (Attenuable (f b) (f a)))
-> Attenuable a b :- Attenuable (f b) (f a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Attenuation (f b) (f a) -> Dict (Attenuable (f b) (f a))
forall k (a :: k) (b :: k).
Attenuation a b -> Dict (Attenuable a b)
toDict (Variance (f b) (f a) a b
forall (f :: * -> *) b a.
(Contravariant f, Representational f) =>
Variance (f b) (f a) a b
contra Attenuation a b
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation))
transitivity
:: forall b a c. (Attenuable b c, Attenuable a b) :- Attenuable a c
transitivity :: (Attenuable b c, Attenuable a b) :- Attenuable a c
transitivity = ((Attenuable b c, Attenuable a b) => Dict (Attenuable a c))
-> (Attenuable b c, Attenuable a b) :- Attenuable a c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (Attenuation a c -> Dict (Attenuable a c)
forall k (a :: k) (b :: k).
Attenuation a b -> Dict (Attenuable a b)
toDict (Attenuation a c -> Dict (Attenuable a c))
-> Attenuation a c -> Dict (Attenuable a c)
forall a b. (a -> b) -> a -> b
$ Attenuable b c => Attenuation b c
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation @b @c Attenuation b c -> Attenuation a b -> Attenuation a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Attenuable a b => Attenuation a b
forall k (a :: k) (b :: k). Attenuable a b => Attenuation a b
attenuation @a @b)
iso :: Attenuation a b -> Attenuation b a -> Coercion a b
iso :: Attenuation a b -> Attenuation b a -> Coercion a b
iso (Attenuation Coercion a b
c) Attenuation b a
_ = Coercion a b
c