-- 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 RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeOperators #-}

-- | 'Attenuation's for 'Profunctor's.

module Data.Type.Attenuation.Profunctor
         ( -- * Profunctor Attenuations
           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)

-- | Lift an 'Attenuation' contravariantly over the left of a 'Profunctor'.
--
-- Similarly to the use of 'Data.Functor.Contravariant.Contravariant' in
-- 'Data.Type.Attenuation.contra', we use 'Profunctor' to guarantee
-- contravariance in the appropriate parameter.
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)

-- | Lift an 'Attenuation' covariantly over the right of a 'Profunctor'.
--
-- Similarly to the use of 'Functor' in 'Data.Type.Attenuation.co', we use
-- 'Profunctor' to guarantee covariance in the appropriate parameter.
--
-- As with 'Data.Type.Attenuation.sndco', this functions the same as
-- 'Data.Type.Attenuation.co', but the needed 'Functor' instance might not be
-- available in polymorphic contexts.
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)

-- 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

-- | 'Profunctor's map attenuations profunctorially.
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))