{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

-- | Free-Tambara product optic packing.
--
-- The promoted canonical shape puts the base arrow first:
--
-- @
-- data Optic arr mon s u a b where
--   Optic :: arr s (mon m a) -> arr (mon m b) u -> Optic arr mon s u a b
-- @
--
-- * @mon@ is the monoidal action on the residual × interface.
-- * @s, u@ are the outer state endpoints (@s -> u@).
-- * @a, b@ are play / coplay (the interface).
--
-- This module is the function-arrow special case (@arr = (->)@):
--
-- @
-- Optic mon s u a b  ≅  ∃m. (s -> mon m a) × (mon m b -> u)
-- @
--
-- Provenance: circuits @examples/tambara.md@ / Milewski /Tambara Equipment/.
--
-- @
-- FreeTamb t j  →  j = Rep a b  →  Optic t  →  t = (,)  →  Lens
-- @
--
-- Residual @m@ is /owned data/ (hinge table cell A). PCA keeps the principal
-- summand as focus and the minor complement as residual — never seals it
-- with 'Circuit.Trace.trace'.
module Circuit.PCA.Optic
  ( Optic (..),
    Lens,
    OneShot,
    fromClassical,
    toClassical,
    view,
    set,
    over,

    -- * Adapter to polynomial morphisms
    morphismAsLens,
    lensAsMorphism,
  )
where

import Circuit.Poly (Mono, Morphism, applyLens, lens)

-- $setup
-- >>> import Circuit.Poly
-- >>> import Circuit.PCA.Optic

-- | Existential residual optic for monoidal action @mon@ over @(->)@.
--
-- The promoted/canonical shape is @Optic arr mon s u a b@; here the base
-- arrow is fixed to @(->)@.
--
-- @
-- Optic mon s u a b  ≅  ∃m. (s -> mon m a) × (mon m b -> u)
-- @
data Optic mon s u a b where
  Optic :: (s -> mon m a) -> (mon m b -> u) -> Optic mon s u a b

-- | Product-action optic = classical lens packing.
--
-- In classical notation the outer ends are named @s, t@ rather than @s, u@.
type Lens s t a b = Optic (,) s t a b

-- | One-shot product-residual optic.
--
-- This is the shape that a single state-changing morphism takes. It is /not/
-- the same as 'Circuit.Poly.System': a 'System' has a fixed carrier and is
-- iterable, whereas a 'OneShot' morphism may change its outer state @s -> u@.
type OneShot s u a b = Optic (,) s u a b

-- | Yoneda form @s -> (a, b -> t)@ into existential residual form.
fromClassical :: (s -> (a, b -> t)) -> Lens s t a b
fromClassical :: forall s a b t. (s -> (a, b -> t)) -> Lens s t a b
fromClassical s -> (a, b -> t)
f =
  (s -> (b -> t, a)) -> ((b -> t, b) -> t) -> Optic (,) s t a b
forall {k} {k} s (mon :: k -> k -> *) (m :: k) (a :: k) (b :: k) u.
(s -> mon m a) -> (mon m b -> u) -> Optic mon s u a b
Optic
    (\s
s -> let (a
a, b -> t
k) = s -> (a, b -> t)
f s
s in (b -> t
k, a
a))
    (\(b -> t
k, b
b) -> b -> t
k b
b)

-- | Existential residual form into Yoneda form.
toClassical :: Lens s t a b -> s -> (a, b -> t)
toClassical :: forall s t a b. Lens s t a b -> s -> (a, b -> t)
toClassical (Optic s -> (m, a)
get (m, b) -> t
put) s
s =
  let (m
m, a
a) = s -> (m, a)
get s
s
   in (a
a, \b
b -> (m, b) -> t
put (m
m, b
b))

-- | Read the focus, discarding residual.
view :: Lens s s a a -> s -> a
view :: forall s a. Lens s s a a -> s -> a
view Lens s s a a
l s
s = (a, a -> s) -> a
forall a b. (a, b) -> a
fst (Lens s s a a -> s -> (a, a -> s)
forall s t a b. Lens s t a b -> s -> (a, b -> t)
toClassical Lens s s a a
l s
s)

-- | Replace the focus, keeping residual from @s@.
set :: Lens s t a b -> b -> s -> t
set :: forall s t a b. Lens s t a b -> b -> s -> t
set Lens s t a b
l b
b s
s = (a, b -> t) -> b -> t
forall a b. (a, b) -> b
snd (Lens s t a b -> s -> (a, b -> t)
forall s t a b. Lens s t a b -> s -> (a, b -> t)
toClassical Lens s t a b
l s
s) b
b

-- | Map the focus.
over :: Lens s t a b -> (a -> b) -> s -> t
over :: forall s t a b. Lens s t a b -> (a -> b) -> s -> t
over Lens s t a b
l a -> b
f s
s =
  let (a
a, b -> t
k) = Lens s t a b -> s -> (a, b -> t)
forall s t a b. Lens s t a b -> s -> (a, b -> t)
toClassical Lens s t a b
l s
s
   in b -> t
k (a -> b
f a
a)

-- ---------------------------------------------------------------------------
-- Adapter: polynomial monomial morphism <-> classical state-preserving lens
-- ---------------------------------------------------------------------------

-- | A polynomial morphism @Mono s s -> Mono i o@ is exactly a state-preserving
-- classical lens @Lens s s o i@.
--
-- Both pack the same data: @s -> (o, i -> s)@.
--
-- >>> let m = lens (\s -> s + 1) (\s i -> s + i) :: Morphism (Mono Int Int) (Mono Int Int)
-- >>> view (morphismAsLens m) 5
-- 6
morphismAsLens :: Morphism (Mono s s) (Mono i o) -> Lens s s o i
morphismAsLens :: forall s i o. Morphism (Mono s s) (Mono i o) -> Lens s s o i
morphismAsLens Morphism (Mono s s) (Mono i o)
m = (s -> (o, i -> s)) -> Lens s s o i
forall s a b t. (s -> (a, b -> t)) -> Lens s t a b
fromClassical ((s -> (o, i -> s)) -> Lens s s o i)
-> (s -> (o, i -> s)) -> Lens s s o i
forall a b. (a -> b) -> a -> b
$ \s
s ->
  let (o
o, i -> s
put) = Morphism (Mono s s) (Mono i o) -> s -> (o, i -> s)
forall da a db b.
Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens Morphism (Mono s s) (Mono i o)
m s
s
   in (o
o, i -> s
put)

-- | Inverse of 'morphismAsLens'.
--
-- >>> let l = fromClassical (\s -> (s * 2, \i -> s + i)) :: Lens Int Int Int Int
-- >>> let m = lensAsMorphism l :: Morphism (Mono Int Int) (Mono Int Int)
-- >>> let (o, put) = applyLens m 5 in (o, put 3)
-- (10,8)
lensAsMorphism :: Lens s s o i -> Morphism (Mono s s) (Mono i o)
lensAsMorphism :: forall s o i. Lens s s o i -> Morphism (Mono s s) (Mono i o)
lensAsMorphism Lens s s o i
l = (s -> o) -> (s -> i -> s) -> Morphism (Mono s s) (Mono i o)
forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens s -> o
get s -> i -> s
put
  where
    get :: s -> o
get s
s = (o, i -> s) -> o
forall a b. (a, b) -> a
fst (Lens s s o i -> s -> (o, i -> s)
forall s t a b. Lens s t a b -> s -> (a, b -> t)
toClassical Lens s s o i
l s
s)
    put :: s -> i -> s
put s
s i
i = (o, i -> s) -> i -> s
forall a b. (a, b) -> b
snd (Lens s s o i -> s -> (o, i -> s)
forall s t a b. Lens s t a b -> s -> (a, b -> t)
toClassical Lens s s o i
l s
s) i
i