-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# 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 #-}

-- | Representational subtyping relations and variance roles.

module Data.Type.Attenuation
         ( -- * Attenuation
           Attenuation, type (:⊆:), attenuateWith, coercible
         , trans, repr, coer, iso, inst
           -- ** Representationality
         , Representational, Representational0, Representational1, Variance
           -- ** Functor and Contravariant
         , co, contra
           -- ** Bifunctor
         , fstco, sndco
           -- ** (->)
         , domain, codomain
           -- ** Initial and Final Objects
         , attVoid, attAny
           -- * Attenuable
         , Attenuable(..), type (⊆), attenuate
         , withAttenuation
           -- ** Entailments
         , 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

-- | An operator form of 'Attenuation', by analogy to (':~:').
type (:⊆:) = Attenuation

-- | Coerce along an 'Attenuation'.
--
-- This is really, truly a coercion when it reaches Core.
attenuateWith :: Attenuation a b -> a -> b
attenuateWith :: Attenuation a b -> a -> b
attenuateWith (Attenuation Coercion a b
Coercion) = a -> b
coerce

-- | Any coercible types have an 'Attenuation'.
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

-- | Any type is unidirectionally coercible to itself.
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

-- | Bidirectional coercions can be weakened to unidirectional coercions.
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

-- | Lift an 'Attenuation' contravariantly over a type constructor @f@.
--
-- Regarding the 'Contravariant' constraint, see 'co', and interchange mentions
-- of covariance and contravariance.
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)

-- | 'Attenuation's across type constructors can be instantiated.
--
-- This means 'Attenuation's across type constructors lift equality of type
-- parameters to 'Attenuation' of the applied result.
--
-- This is analogous to how @Coercible f g@ works.
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

-- | 'Attenuation' of 'Void' to any type.
--
-- If you have 'Void' appearing covariantly in a type, you can replace it with
-- any other lifted type with a coercion, because the value can't contain any
-- non-bottom 'Void' values (there are none), and any value that /is/ bottom
-- can "work" (i.e. throw or fail to terminate) just as well at any other
-- lifted type.
--
-- For example, if you have a @[Doc Void]@ (from
-- <https://hackage.haskell.org/package/pretty pretty>), you know it doesn't
-- have any annotations (or they're errors), so you can use it as @[Doc a]@
-- without actually traversing the list and @Doc@ structure to apply
-- 'Data.Void.absurd' to all of the 'Void's.
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

-- | 'Attenuation' of any type to 'Any'.
--
-- Similarly to 'attVoid', you can weaken any type to 'Any' for free, since any
-- value is a valid value of type 'Any'.
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

-- | An operator form of 'Attenuable'.
type (⊆) = Attenuable

-- | Coerce from a representational subtype @a@ to its supertype @b@.
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

-- Type inference aid for use in entailments: otherwise it's ambiguous what
-- 'Attenuation' we want to promote with 'withAttenuation'.
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

-- | 'Contravariant' functors map attenuation contravariantly.
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))

-- | 'Attenuation's are transitive.
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)

-- | If 'Attenuation's in both directions exist, they're actually a 'Coercion'.
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