-- | Mixed optics as residual maps.
--
-- In the equipment-optics story an optic between two spans with common
-- boundaries is a globular 2-cell between the corresponding loose arrows.  In
-- @Prof@ that unwinds to the mixed-optic coend
--
-- @
--   Optic_M((S,R),(A,B)) = ∫^M C(S, M ⊙ A) × D(M ⊙ B, R)
-- @
--
-- where @⊙@ is a monoidal action.  In @circuits@ the action is the tensor @t@
-- itself.  'Optic' is the /integrand/ — the residual @ch@ is in the type, so
-- this is the residual-remembering rung.  'SomeOptic' hides it, which is the
-- coend without the quotient.
--
-- == Relationship to the rest of the library
--
-- 'Optic' is the curried form of 'Circuit.Poles.iomap': an optic is exactly a
-- pair of actions on channel poles, 'Circuit.Poles.prefixIn' on the conjoint
-- and 'Circuit.Poles.suffixOut' on the companion.  'opticPoles' is that
-- identification, and it costs nothing to state.
--
-- The objects of the optic category are boundary /pairs/, which the local
-- 'Circuit.Category.Category' class cannot index directly.  "Circuit.Poly"
-- already solves that problem: @'Circuit.Poly.Mono' i o@ packages a boundary
-- pair as a single @Poly@, and @instance Category Morphism@ is the wiki's
-- "category for free".  So this module does not duplicate that instance; it
-- maps into it, with 'opticAsLens' and 'lensAsOptic'.
--
-- == Constraints
--
-- Only 'identityOptic' needs 'Unital', for the unitors.  Composition and the
-- update action need nothing beyond 'Strength', because
-- @'strength' f == 'Circuit.Tensor.tensor' 'Circuit.Category.id' f@ — a
-- coherence the @Axioma.Circ@ oracles check at @(,)@, 'Either' and 'These'.
-- This matters for base arrows that are premonoidal and therefore have
-- 'Strength' but deliberately no 'Tensor' instance, such as @Circuit.Prob@.
module Circuit.Optic
  ( -- * Mixed optic
    Optic (..),
    SomeOptic (..),
    withSomeOptic,

    -- * Composition
    identityOptic,
    composeOptic,
    identitySomeOptic,
    composeSomeOptic,

    -- * Action on morphisms
    opticUpdate,
    someOpticUpdate,

    -- * Action on channel poles
    opticPoles,

    -- * Bridge to the polynomial lens
    opticAsLens,
    lensAsOptic,
  )
where

import Circuit.Category (Category, (.>))
import Circuit.Channel (Channel (..), Strength (..))
import Circuit.Poles (Poles, iomap)
import Circuit.Poly (Mono, Morphism, applyLens, lens)
import Circuit.Tensor (Unit, Unital (..))
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Optic
-- >>> import Circuit.Poles (Poles, poles0, splay0)
-- >>> import Circuit.Poly (applyLens)
-- >>> import Prelude hiding (id, (.))
-- >>> :{
-- let firstLens :: Optic (,) (->) String Int Int (Int, String) (Int, String)
--     firstLens = Optic (\(n, s) -> (s, n)) (\(s, n) -> (n, s))
--     outer :: Optic (,) (->) String (Int, Bool) (Int, Bool) ((Int, Bool), String) ((Int, Bool), String)
--     outer = Optic (\(p, s) -> (s, p)) (\(s, p) -> (p, s))
--     inner :: Optic (,) (->) Bool Int Int (Int, Bool) (Int, Bool)
--     inner = Optic (\(n, b) -> (b, n)) (\(b, n) -> (n, b))
--     prismLeft :: Optic Either (->) String Int Int (Either Int String) (Either Int String)
--     prismLeft =
--       Optic
--         (\case { Left n -> Right n; Right s -> Left s })
--         (\case { Left s -> Right s; Right n -> Left n })
-- :}

-- | A mixed optic from @(s,r)@ to @(a,b)@ with residual @ch@.
--
-- * @opticForward :: arr s (t ch a)@ splits the domain left boundary into the
--   residual and the codomain left boundary.
-- * @opticBackward :: arr (t ch b) r@ recombines the residual with the
--   codomain right boundary.
--
-- For @t = (,)@ and @arr = (->)@ this is the concrete lens pair
-- @s -> (ch, a)@ and @(ch, b) -> r@.  For @t = 'Either'@ it is a prism: the
-- residual is the branch that did not match.
data Optic t arr ch a b s r = Optic
  { -- | Forward direction: introduce the residual and the codomain left boundary.
    forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
Optic t arr ch a b s r -> arr s (t ch a)
opticForward :: arr s (t ch a),
    -- | Backward direction: consume the residual and the codomain right boundary.
    forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
Optic t arr ch a b s r -> arr (t ch b) r
opticBackward :: arr (t ch b) r
  }

-- | A mixed optic with the residual existentially hidden.
--
-- There is no residual /value/ here, only a residual type: the forward leg
-- produces the residual and the backward leg consumes it.  This is why
-- 'SomeOptic' is cheaper than 'Circuit.Body.SomeBody', which must store a
-- seed and therefore has no inhabitant at tensors with an uninhabited unit.
-- 'identitySomeOptic' exists at 'Either', where @'Circuit.Tensor.Unit'
-- 'Either' = 'Data.Void.Void'@ and the corresponding @SomeBody@ identity does
-- not.
data SomeOptic t arr a b s r where
  SomeOptic :: Optic t arr ch a b s r -> SomeOptic t arr a b s r

-- | Eliminator for the existential residual type.
withSomeOptic ::
  SomeOptic t arr a b s r ->
  (forall ch. Optic t arr ch a b s r -> x) ->
  x
withSomeOptic :: forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (s :: k) (r :: k) x.
SomeOptic t arr a b s r
-> (forall (ch :: k). Optic t arr ch a b s r -> x) -> x
withSomeOptic (SomeOptic Optic t arr ch a b s r
o) forall (ch :: k). Optic t arr ch a b s r -> x
k = Optic t arr ch a b s r -> x
forall (ch :: k). Optic t arr ch a b s r -> x
k Optic t arr ch a b s r
o

-- | Identity optic at the boundary pair @(a,b)@.  The residual is the tensor
-- unit.
--
-- This is the only operation in the module that needs 'Unital' rather than
-- 'Strength', and it needs only the unitors.
identityOptic :: (Unital t arr) => Optic t arr (Unit t) a b a b
identityOptic :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Unital t arr =>
Optic t arr (Unit t) a b a b
identityOptic = arr a (t (Unit t) a)
-> arr (t (Unit t) b) b -> Optic t arr (Unit t) a b a b
forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
arr s (t ch a) -> arr (t ch b) r -> Optic t arr ch a b s r
Optic arr a (t (Unit t) a)
forall (a :: k). arr a (t (Unit t) a)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr a (t (Unit t) a)
unitl' arr (t (Unit t) b) b
forall (a :: k). arr (t (Unit t) a) a
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k).
Unital t arr =>
arr (t (Unit t) a) a
unitl
{-# INLINE identityOptic #-}

-- | Vertical composition of mixed optics.
--
-- Given @opt1@ from @(s,r)@ to @(a,b)@ with residual @ch1@ and @opt2@ from
-- @(a,b)@ to @(u,v)@ with residual @ch2@, the composite has residual
-- @t ch1 ch2@ — the tensoring of residuals in the coend formula.  The
-- residual order matches 'Circuit.Body.cascadeBody': first-applied on the
-- left.
--
-- Note what is /absent/: composition reassociates and applies 'strength', but
-- never 'Circuit.Channel.slide'.  'Circuit.Body.cascadeBody' needs two slides,
-- because a single 'Circuit.Body.Body' must push one carrier past the payload
-- so that one arrow sees both.  An optic keeps its two residuals on the same
-- side throughout.  That is the precise sense in which body composition is the
-- fused case of optic composition.
--
-- Unit and associativity hold only up to the residual unitor and associator,
-- exactly as for 'Circuit.Circ.Circ'; the observational statements are in
-- @Axioma.Optic@.
--
-- >>> opticUpdate (composeOptic inner outer) (+ 1) ((3, True), "hi")
-- ((4,True),"hi")
--
-- The same result by nesting the updates — functoriality of 'opticUpdate':
--
-- >>> opticUpdate outer (opticUpdate inner (+ 1)) ((3, True), "hi")
-- ((4,True),"hi")
composeOptic ::
  (Strength t arr) =>
  Optic t arr ch2 u v a b ->
  Optic t arr ch1 a b s r ->
  Optic t arr (t ch1 ch2) u v s r
composeOptic :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch2 :: k)
       (u :: k) (v :: k) (a :: k) (b :: k) (ch1 :: k) (s :: k) (r :: k).
Strength t arr =>
Optic t arr ch2 u v a b
-> Optic t arr ch1 a b s r -> Optic t arr (t ch1 ch2) u v s r
composeOptic (Optic arr a (t ch2 u)
f2 arr (t ch2 v) b
b2) (Optic arr s (t ch1 a)
f1 arr (t ch1 b) r
b1) =
  arr s (t (t ch1 ch2) u)
-> arr (t (t ch1 ch2) v) r -> Optic t arr (t ch1 ch2) u v s r
forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
arr s (t ch a) -> arr (t ch b) r -> Optic t arr ch a b s r
Optic
    (arr s (t ch1 a)
f1 arr s (t ch1 a)
-> arr (t ch1 a) (t ch1 (t ch2 u)) -> arr s (t ch1 (t ch2 u))
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr a (t ch2 u) -> arr (t ch1 a) (t ch1 (t ch2 u))
forall (b :: k) (c :: k) (a :: k). arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength arr a (t ch2 u)
f2 arr s (t ch1 (t ch2 u))
-> arr (t ch1 (t ch2 u)) (t (t ch1 ch2) u)
-> arr s (t (t ch1 ch2) u)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch1 (t ch2 u)) (t (t ch1 ch2) u)
forall (a :: k) (b :: k) (c :: k). arr (t a (t b c)) (t (t a b) c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc')
    (arr (t (t ch1 ch2) v) (t ch1 (t ch2 v))
forall (a :: k) (b :: k) (c :: k). arr (t (t a b) c) (t a (t b c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc arr (t (t ch1 ch2) v) (t ch1 (t ch2 v))
-> arr (t ch1 (t ch2 v)) (t ch1 b)
-> arr (t (t ch1 ch2) v) (t ch1 b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch2 v) b -> arr (t ch1 (t ch2 v)) (t ch1 b)
forall (b :: k) (c :: k) (a :: k). arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength arr (t ch2 v) b
b2 arr (t (t ch1 ch2) v) (t ch1 b)
-> arr (t ch1 b) r -> arr (t (t ch1 ch2) v) r
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch1 b) r
b1)
{-# INLINE composeOptic #-}

-- | 'identityOptic' with the residual hidden.
identitySomeOptic :: (Unital t arr) => SomeOptic t arr a b a b
identitySomeOptic :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Unital t arr =>
SomeOptic t arr a b a b
identitySomeOptic = Optic t arr (Unit t) a b a b -> SomeOptic t arr a b a b
forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
Optic t arr ch a b s r -> SomeOptic t arr a b s r
SomeOptic Optic t arr (Unit t) a b a b
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k).
Unital t arr =>
Optic t arr (Unit t) a b a b
identityOptic
{-# INLINE identitySomeOptic #-}

-- | 'composeOptic' with the residuals hidden.  Once hidden, the bracketing
-- that makes 'composeOptic' associative only up to the associator is no longer
-- observable in the type.
composeSomeOptic ::
  (Strength t arr) =>
  SomeOptic t arr u v a b ->
  SomeOptic t arr a b s r ->
  SomeOptic t arr u v s r
composeSomeOptic :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (u :: k)
       (v :: k) (a :: k) (b :: k) (s :: k) (r :: k).
Strength t arr =>
SomeOptic t arr u v a b
-> SomeOptic t arr a b s r -> SomeOptic t arr u v s r
composeSomeOptic (SomeOptic Optic t arr ch u v a b
o2) (SomeOptic Optic t arr ch a b s r
o1) = Optic t arr (t ch ch) u v s r -> SomeOptic t arr u v s r
forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
Optic t arr ch a b s r -> SomeOptic t arr a b s r
SomeOptic (Optic t arr ch u v a b
-> Optic t arr ch a b s r -> Optic t arr (t ch ch) u v s r
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch2 :: k)
       (u :: k) (v :: k) (a :: k) (b :: k) (ch1 :: k) (s :: k) (r :: k).
Strength t arr =>
Optic t arr ch2 u v a b
-> Optic t arr ch1 a b s r -> Optic t arr (t ch1 ch2) u v s r
composeOptic Optic t arr ch u v a b
o2 Optic t arr ch a b s r
o1)
{-# INLINE composeSomeOptic #-}

-- | Apply an optic to a plain base-arrow morphism.
--
-- A lens turns a focus-update into a whole-update; a prism turns a
-- branch-update into a sum-update.
--
-- >>> opticUpdate firstLens (+ 1) (3, "hello")
-- (4,"hello")
--
-- >>> (opticUpdate prismLeft (+ 1) (Left 3), opticUpdate prismLeft (+ 1) (Right "hi"))
-- (Left 4,Right "hi")
--
-- Lawfulness is not enforced.  @'opticUpdate' o 'Circuit.Category.id' ==
-- 'Circuit.Category.id'@ is the round-trip condition, and a well-typed optic
-- can fail it; @Axioma.Optic@ carries a witness that it can.
opticUpdate ::
  (Strength t arr) =>
  Optic t arr ch a b s r ->
  arr a b ->
  arr s r
opticUpdate :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch :: k)
       (a :: k) (b :: k) (s :: k) (r :: k).
Strength t arr =>
Optic t arr ch a b s r -> arr a b -> arr s r
opticUpdate (Optic arr s (t ch a)
f arr (t ch b) r
b) arr a b
m = arr s (t ch a)
f arr s (t ch a) -> arr (t ch a) (t ch b) -> arr s (t ch b)
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr a b -> arr (t ch a) (t ch b)
forall (b :: k) (c :: k) (a :: k). arr b c -> arr (t a b) (t a c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (b :: k)
       (c :: k) (a :: k).
Strength t arr =>
arr b c -> arr (t a b) (t a c)
strength arr a b
m arr s (t ch b) -> arr (t ch b) r -> arr s r
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr (t ch b) r
b
{-# INLINE opticUpdate #-}

-- | 'opticUpdate' through the existential.
someOpticUpdate ::
  (Strength t arr) =>
  SomeOptic t arr a b s r ->
  arr a b ->
  arr s r
someOpticUpdate :: forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (s :: k) (r :: k).
Strength t arr =>
SomeOptic t arr a b s r -> arr a b -> arr s r
someOpticUpdate (SomeOptic Optic t arr ch a b s r
o) = Optic t arr ch a b s r -> arr a b -> arr s r
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (ch :: k)
       (a :: k) (b :: k) (s :: k) (r :: k).
Strength t arr =>
Optic t arr ch a b s r -> arr a b -> arr s r
opticUpdate Optic t arr ch a b s r
o
{-# INLINE someOpticUpdate #-}

-- | The action of an optic on channel poles.
--
-- This is 'Circuit.Poles.iomap' with its two arguments read as the legs of an
-- optic: 'opticForward' prefixes the conjoint, 'opticBackward' suffixes the
-- companion.  Since "Circuit.Poles" already describes that pair as "the left
-- action of @arr@ on @In@ poles" and "the right action of @arr@ on @Out@
-- poles", an optic /is/ a morphism of that enriched profunctor.
--
-- >>> let p = poles0 (const ()) (const ("hi", 7)) :: Poles (->) (String, Int) (String, Int)
-- >>> snd (splay0 (opticPoles firstLens p)) ()
-- (7,"hi")
opticPoles ::
  (Category arr) =>
  Optic t arr ch a b s r ->
  Poles arr (t ch a) (t ch b) ->
  Poles arr s r
opticPoles :: forall {k1} {k} {k} (arr :: k1 -> k1 -> *) (t :: k -> k -> k1)
       (ch :: k) (a :: k) (b :: k) (s :: k1) (r :: k1).
Category arr =>
Optic t arr ch a b s r
-> Poles arr (t ch a) (t ch b) -> Poles arr s r
opticPoles (Optic arr s (t ch a)
f arr (t ch b) r
b) = arr s (t ch a)
-> arr (t ch b) r -> Poles arr (t ch a) (t ch b) -> Poles arr s r
forall {k} (arr :: k -> k -> *) (a :: k) (a' :: k) (b :: k)
       (b' :: k).
Category arr =>
arr a' a -> arr b b' -> Poles arr a b -> Poles arr a' b'
iomap arr s (t ch a)
f arr (t ch b) r
b
{-# INLINE opticPoles #-}

-- | A cartesian optic as a polynomial lens.
--
-- Currying the residual away turns the pair @s -> (ch, a)@, @(ch, b) -> r@
-- into @s -> (a, b -> r)@, which is exactly
-- @'Circuit.Poly.applyLens' :: 'Morphism' ('Mono' r s) ('Mono' b a) -> s -> (a, b -> r)@.
--
-- >>> let (a, put) = applyLens (opticAsLens (SomeOptic firstLens)) (3, "hello") in (a, put 9)
-- (3,(9,"hello"))
opticAsLens :: SomeOptic (,) (->) a b s r -> Morphism (Mono r s) (Mono b a)
opticAsLens :: forall a b s r.
SomeOptic (,) (->) a b s r -> Morphism (Mono r s) (Mono b a)
opticAsLens (SomeOptic (Optic s -> (ch, a)
f (ch, b) -> r
g)) =
  (s -> a) -> (s -> b -> r) -> Morphism (Mono r s) (Mono b a)
forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens (\s
s -> (ch, a) -> a
forall a b. (a, b) -> b
snd (s -> (ch, a)
f s
s)) (\s
s b
b -> (ch, b) -> r
g ((ch, a) -> ch
forall a b. (a, b) -> a
fst (s -> (ch, a)
f s
s), b
b))

-- | A polynomial lens as a cartesian optic.
--
-- The residual is reconstructed as the continuation type @b -> r@ — the
-- classical "existential is a function" encoding.  So @'lensAsOptic'
-- . 'opticAsLens'@ changes the residual and is only an identity after the
-- coend quotient; @Axioma.Optic@ checks that it is an identity
-- observationally, which is that quotient in action.
lensAsOptic :: Morphism (Mono r s) (Mono b a) -> Optic (,) (->) (b -> r) a b s r
lensAsOptic :: forall r s b a.
Morphism (Mono r s) (Mono b a) -> Optic (,) (->) (b -> r) a b s r
lensAsOptic Morphism (Mono r s) (Mono b a)
m =
  (s -> (b -> r, a))
-> ((b -> r, b) -> r) -> Optic (,) (->) (b -> r) a b s r
forall {k} {k} {k} (t :: k -> k -> k) (arr :: k -> k -> *)
       (ch :: k) (a :: k) (b :: k) (s :: k) (r :: k).
arr s (t ch a) -> arr (t ch b) r -> Optic t arr ch a b s r
Optic
    (\s
s -> let (a
a, b -> r
k) = Morphism (Mono r s) (Mono b a) -> s -> (a, b -> r)
forall da a db b.
Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens Morphism (Mono r s) (Mono b a)
m s
s in (b -> r
k, a
a))
    (\(b -> r
k, b
b) -> b -> r
k b
b)