{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
module Fresnel.Profunctor.Coexp
( -- * Coexponential profunctor
  Coexp(..)
  -- * Construction
, coexp
  -- * Elimination
, recall
, forget
) where

import Data.Profunctor
import Data.Profunctor.Unsafe
import Data.Coerce

-- Coexponential

-- | Coexponentials are the dual of functions, consisting of an argument of type @a@ (derived within an environment of type @s@) and a continuation from the return type @b@ (extending to the eventual result type @t@). As such, they naturally have the shape of optics, relating the outer context @s -> t@ to the inner @a -> b@.
newtype Coexp s t b a = Coexp { forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp :: forall r . ((s -> a) -> (b -> t) -> r) -> r }

instance Functor (Coexp s t b) where
  fmap :: forall a b. (a -> b) -> Coexp s t b a -> Coexp s t b b
fmap = (a -> b) -> Coexp s t b a -> Coexp s t b b
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap

instance Monoid t => Applicative (Coexp s t b) where
  pure :: forall a. a -> Coexp s t b a
pure a
a = (s -> a) -> (b -> t) -> Coexp s t b a
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp (a -> s -> a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a) b -> t
forall a. Monoid a => a
mempty
  Coexp s t b (a -> b)
f <*> :: forall a b. Coexp s t b (a -> b) -> Coexp s t b a -> Coexp s t b b
<*> Coexp s t b a
a = Coexp s t b (a -> b)
-> forall r. ((s -> a -> b) -> (b -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t b (a -> b)
f (((s -> a -> b) -> (b -> t) -> Coexp s t b b) -> Coexp s t b b)
-> ((s -> a -> b) -> (b -> t) -> Coexp s t b b) -> Coexp s t b b
forall a b. (a -> b) -> a -> b
$ \ s -> a -> b
f b -> t
kf -> Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t b a
a (((s -> a) -> (b -> t) -> Coexp s t b b) -> Coexp s t b b)
-> ((s -> a) -> (b -> t) -> Coexp s t b b) -> Coexp s t b b
forall a b. (a -> b) -> a -> b
$ \ s -> a
a b -> t
ka -> (s -> b) -> (b -> t) -> Coexp s t b b
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp (s -> a -> b
f (s -> a -> b) -> (s -> a) -> s -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> s -> a
a) (t -> t -> t
forall a. Monoid a => a -> a -> a
mappend (t -> t -> t) -> (b -> t) -> b -> t -> t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> t
kf (b -> t -> t) -> (b -> t) -> b -> t
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> t
ka)

instance Profunctor (Coexp s t) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Coexp s t b c -> Coexp s t a d
dimap a -> b
f c -> d
g Coexp s t b c
c = Coexp s t b c -> forall r. ((s -> c) -> (b -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t b c
c (((s -> c) -> (b -> t) -> Coexp s t a d) -> Coexp s t a d)
-> ((s -> c) -> (b -> t) -> Coexp s t a d) -> Coexp s t a d
forall a b. (a -> b) -> a -> b
$ \ s -> c
recall b -> t
forget -> (s -> d) -> (a -> t) -> Coexp s t a d
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp (c -> d
g (c -> d) -> (s -> c) -> s -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> c
recall) (b -> t
forget (b -> t) -> (a -> b) -> a -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
  lmap :: forall a b c. (a -> b) -> Coexp s t b c -> Coexp s t a c
lmap a -> b
f Coexp s t b c
c = Coexp s t b c -> forall r. ((s -> c) -> (b -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t b c
c (((s -> c) -> (b -> t) -> Coexp s t a c) -> Coexp s t a c)
-> ((s -> c) -> (b -> t) -> Coexp s t a c) -> Coexp s t a c
forall a b. (a -> b) -> a -> b
$ \ s -> c
recall b -> t
forget -> (s -> c) -> (a -> t) -> Coexp s t a c
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp s -> c
recall (b -> t
forget (b -> t) -> (a -> b) -> a -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
  rmap :: forall b c a. (b -> c) -> Coexp s t a b -> Coexp s t a c
rmap b -> c
g Coexp s t a b
c = Coexp s t a b -> forall r. ((s -> b) -> (a -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t a b
c (((s -> b) -> (a -> t) -> Coexp s t a c) -> Coexp s t a c)
-> ((s -> b) -> (a -> t) -> Coexp s t a c) -> Coexp s t a c
forall a b. (a -> b) -> a -> b
$ \ s -> b
recall a -> t
forget -> (s -> c) -> (a -> t) -> Coexp s t a c
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp (b -> c
g (b -> c) -> (s -> b) -> s -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> b
recall) a -> t
forget
  #. :: forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> Coexp s t a b -> Coexp s t a c
(#.) = (Coexp s t a b -> Coexp s t a c)
-> q b c -> Coexp s t a b -> Coexp s t a c
forall a b. a -> b -> a
const Coexp s t a b -> Coexp s t a c
coerce
  .# :: forall a b c (q :: * -> * -> *).
Coercible b a =>
Coexp s t b c -> q a b -> Coexp s t a c
(.#) = (Coexp s t b c -> Coexp s t a c)
-> (q a b -> Coexp s t b c) -> q a b -> Coexp s t a c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Coexp s t b c -> Coexp s t a c
coerce ((q a b -> Coexp s t b c) -> q a b -> Coexp s t a c)
-> (Coexp s t b c -> q a b -> Coexp s t b c)
-> Coexp s t b c
-> q a b
-> Coexp s t a c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coexp s t b c -> q a b -> Coexp s t b c
forall a b. a -> b -> a
const

instance Semigroup (Coexp a b b a) where
  Coexp a b b a
c1 <> :: Coexp a b b a -> Coexp a b b a -> Coexp a b b a
<> Coexp a b b a
c2 = Coexp a b b a -> forall r. ((a -> a) -> (b -> b) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp a b b a
c1 (((a -> a) -> (b -> b) -> Coexp a b b a) -> Coexp a b b a)
-> ((a -> a) -> (b -> b) -> Coexp a b b a) -> Coexp a b b a
forall a b. (a -> b) -> a -> b
$ \ a -> a
r1 b -> b
f1 -> Coexp a b b a -> forall r. ((a -> a) -> (b -> b) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp a b b a
c2 (((a -> a) -> (b -> b) -> Coexp a b b a) -> Coexp a b b a)
-> ((a -> a) -> (b -> b) -> Coexp a b b a) -> Coexp a b b a
forall a b. (a -> b) -> a -> b
$ \ a -> a
r2 b -> b
f2 -> (a -> a) -> (b -> b) -> Coexp a b b a
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp (a -> a
r2 (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
r1) (b -> b
f1 (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
f2)

instance Monoid (Coexp a b b a) where
  mempty :: Coexp a b b a
mempty = (a -> a) -> (b -> b) -> Coexp a b b a
forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp a -> a
forall a. a -> a
id b -> b
forall a. a -> a
id


-- Construction

coexp :: (s -> a) -> (b -> t) -> Coexp s t b a
coexp :: forall s a b t. (s -> a) -> (b -> t) -> Coexp s t b a
coexp s -> a
recall b -> t
forget = (forall r. ((s -> a) -> (b -> t) -> r) -> r) -> Coexp s t b a
forall s t b a.
(forall r. ((s -> a) -> (b -> t) -> r) -> r) -> Coexp s t b a
Coexp (\ (s -> a) -> (b -> t) -> r
k -> (s -> a) -> (b -> t) -> r
k s -> a
recall b -> t
forget)


-- Elimination

recall :: Coexp s t b a -> (s -> a)
recall :: forall s t b a. Coexp s t b a -> s -> a
recall Coexp s t b a
c = Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t b a
c (s -> a) -> (b -> t) -> s -> a
forall a b. a -> b -> a
const

forget :: Coexp s t b a -> (b -> t)
forget :: forall s t b a. Coexp s t b a -> b -> t
forget Coexp s t b a
c = Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
forall s t b a.
Coexp s t b a -> forall r. ((s -> a) -> (b -> t) -> r) -> r
withCoexp Coexp s t b a
c (((b -> t) -> b -> t) -> (s -> a) -> (b -> t) -> b -> t
forall a b. a -> b -> a
const (b -> t) -> b -> t
forall a. a -> a
id)