{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- \$composition-product, $tensor-wiring.

-- | Sketch: the category Poly.
--
-- Polynomial objects are syntactic expressions, promoted to a kind:
--
--     p, q ::= Y              the identity polynomial
--           |  Const A        a constant set
--           |  Exp A          y^A
--           |  Sum p q        coproduct
--           |  Prod p q       cartesian product
--           |  Tensor p q     Dirichlet/parallel product
--           |  Comp p q       composition (substitution)
--
-- The kind @Poly@ is promoted, so polynomial expressions live at the type
-- level.  'Eval' is a GADT that witnesses the value shape of @p(x)@.  We use
-- a GADT rather than a type family because 'Eval' is not injective in @x@;
-- the GADT lets GHC keep track of the evaluation variable without ambiguity.
--
-- Morphisms are natural transformations between the induced polynomial
-- functors, equivalently bundle maps (positions forward, directions
-- backward).
--
-- Two extra constructors make dependent lenses expressible:
--
-- * 'Konst' introduces a global element (a constant position).
-- * 'Depend' is the copower universal property: a @Const a@-indexed family
--   of morphisms @p -> q@.
--
-- With them, the general point-dependent lens @(get :: a -> b, put :: a -> db -> da)@
-- is a two-line 'Morphism'.
--
-- The 'Tensor' constructor adds the Dirichlet (parallel) product. It requires
-- 'Pos' and 'Dir' type families because a value of @(p ⊗ q)(x)@ is a pair of
-- positions together with a single function out of the product of direction
-- sets — not derivable from a pair of ordinary 'Eval' values.
--
-- Worked examples: $netlist-view, $netlist-roundtrip, $dirichlet-tensor,
module Circuit.Poly
  ( -- * Polynomial expressions
    Poly (..),
    Eval (..),

    -- * Positions and directions
    Pos,
    Dir,

    -- * Netlist view
    Netlist (..),
    netRoundTrip,
    tensorUnitorL,
    tensorUnitorL',
    tensorUnitorR,
    tensorUnitorR',

    -- * Tensor functoriality
    morphAt,
    parT,

    -- * Composition product
    nestedToComp,
    compToNested,
    compUnitorL,
    compUnitorL',
    compUnitorR,
    compUnitorR',
    compAssocL,
    compAssocR,

    -- * Tensor wiring
    tensorEval,

    -- * Morphisms
    Morphism (..),
    runMorphism,

    -- * Lenses
    Mono,
    lens,
    dagger,
    applyLens,

    -- * Prisms
    prism,
    prismMatch,
  )
where

import Circuit.Category (Category (..), (.>))
import Data.Bifunctor
import Data.Kind (Type)
import Data.Void (Void, absurd)
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Category (id, (.))
-- >>> import Circuit.Poly
-- >>> import Prelude hiding (id, (.))

-- | Syntactic polynomial objects, promoted to a kind.
data Poly
  = Y
  | Const Type
  | Exp Type
  | Sum Poly Poly
  | Prod Poly Poly
  | Tensor Poly Poly
  | Comp Poly Poly

-- | Position set of a polynomial.
--
-- For a value of @p(x)@, 'Pos p' is the index type of positions.
type family Pos (p :: Poly) :: Type where
  Pos 'Y = ()
  Pos ('Const a) = a
  Pos ('Exp a) = ()
  Pos ('Sum p q) = Either (Pos p) (Pos q)
  Pos ('Prod p q) = (Pos p, Pos q)
  Pos ('Tensor p q) = (Pos p, Pos q)
  Pos ('Comp p q) = (Pos p, Dir p -> Pos q)

-- | Direction set of a polynomial.
--
-- For a value of @p(x)@ at a given position, 'Dir p' is the domain of the
-- function into @x@.
--
-- 'Sum' gets a /flat/ direction space @'Either' ('Dir' p) ('Dir' q)@.  This
-- is an over-approximation: only the branch selected by the position is
-- in-fibre.  It is nonetheless the right shape for /dynamics/, where the
-- input direction is supplied after the position is observed: a wrong-branch
-- direction is simply off-fibre.  The netlist view ('Netlist') remains
-- position-dependent and still does not admit a 'Sum' instance.
--
-- For 'Comp', @'Dir' ('Comp p q) = ('Dir p, 'Dir q)@ is the same flat
-- approximation: the @q@-position (hence its honest pin set) depends on which
-- @p@-direction was taken.  Exact for Sum-free factors with uniform
-- directions — the monomial fragment.
type family Dir (p :: Poly) :: Type where
  Dir 'Y = ()
  Dir ('Const a) = Void
  Dir ('Exp a) = a
  Dir ('Sum p q) = Either (Dir p) (Dir q)
  Dir ('Prod p q) = Either (Dir p) (Dir q)
  Dir ('Tensor p q) = (Dir p, Dir q)
  Dir ('Comp p q) = (Dir p, Dir q)

-- | Values of a polynomial functor @p@ evaluated at @x@.
--
-- The constructors mirror the polynomial grammar.  'EP' and 'ES' wrap the
-- standard product and coproduct of Haskell (@(,)@ and 'Either'); they are
-- not reimplemented, only tagged so that the polynomial shape remains
-- inspectable.
--
-- 'ET' is the Dirichlet tensor: a pair of positions with one function out of
-- the product of direction sets. This cannot be built from a pair of ordinary
-- 'Eval' values, which is why 'Pos' and 'Dir' are needed.
--
-- 'EC' is the composition product: a @p@-position with a @q@-component hung on
-- each @p@-pin, and a path @(dp, dq)@ into @x@.
data Eval (p :: Poly) (x :: Type) where
  EY :: x -> Eval 'Y x
  EK :: c -> Eval ('Const c) x
  EE :: (a -> x) -> Eval ('Exp a) x
  ES :: Either (Eval p x) (Eval q x) -> Eval ('Sum p q) x
  EP :: (Eval p x, Eval q x) -> Eval ('Prod p q) x
  ET :: (Pos p, Pos q) -> ((Dir p, Dir q) -> x) -> Eval ('Tensor p q) x
  EC ::
    (Pos p, Dir p -> Pos q) ->
    ((Dir p, Dir q) -> x) ->
    Eval ('Comp p q) x

instance Functor (Eval p) where
  fmap :: forall a b. (a -> b) -> Eval p a -> Eval p b
fmap a -> b
f = \case
    EY a
x -> b -> Eval 'Y b
forall x. x -> Eval 'Y x
EY (a -> b
f a
x)
    EK c
c -> c -> Eval ('Const c) b
forall p x. p -> Eval ('Const p) x
EK c
c
    EE a -> a
g -> (a -> b) -> Eval ('Exp a) b
forall p x. (p -> x) -> Eval ('Exp p) x
EE (a -> b
f (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> a
g)
    ES Either (Eval p a) (Eval q a)
e -> Either (Eval p b) (Eval q b) -> Eval ('Sum p q) b
forall (p :: Poly) x (b :: Poly).
Either (Eval p x) (Eval b x) -> Eval ('Sum p b) x
ES ((Eval p a -> Eval p b)
-> (Eval q a -> Eval q b)
-> Either (Eval p a) (Eval q a)
-> Either (Eval p b) (Eval q b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((a -> b) -> Eval p a -> Eval p b
forall a b. (a -> b) -> Eval p a -> Eval p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ((a -> b) -> Eval q a -> Eval q b
forall a b. (a -> b) -> Eval q a -> Eval q b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) Either (Eval p a) (Eval q a)
e)
    EP (Eval p a
a, Eval q a
b) -> (Eval p b, Eval q b) -> Eval ('Prod p q) b
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP ((a -> b) -> Eval p a -> Eval p b
forall a b. (a -> b) -> Eval p a -> Eval p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Eval p a
a, (a -> b) -> Eval q a -> Eval q b
forall a b. (a -> b) -> Eval q a -> Eval q b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Eval q a
b)
    ET (Pos p, Pos q)
pos (Dir p, Dir q) -> a
g -> (Pos p, Pos q) -> ((Dir p, Dir q) -> b) -> Eval ('Tensor p q) b
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET (Pos p, Pos q)
pos (a -> b
f (a -> b) -> ((Dir p, Dir q) -> a) -> (Dir p, Dir q) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (Dir p, Dir q) -> a
g)
    EC (Pos p, Dir p -> Pos q)
pos (Dir p, Dir q) -> a
g -> (Pos p, Dir p -> Pos q)
-> ((Dir p, Dir q) -> b) -> Eval ('Comp p q) b
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC (Pos p, Dir p -> Pos q)
pos (a -> b
f (a -> b) -> ((Dir p, Dir q) -> a) -> (Dir p, Dir q) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (Dir p, Dir q) -> a
g)

-- $netlist-view
--
-- Polynomials that admit a netlist view: every value is a chosen position
-- together with an assignment of that position's pins (directions) into @x@.
--
-- The view is defined structurally over the promoted grammar. It is the
-- missing inverse that lets us build arbitrary 'Eval' values from netlist
-- data — in particular it underlies the unitors for the Dirichlet tensor
-- and the functorial action @parT@ on tensor factors.
--
-- 'Sum' is deliberately /not/ an instance. A sum value stores its pin set
-- in the branch constructor ('ES'), so there is no single flat direction
-- set 'Dir' can assign to it. That is the honest boundary of the view;
-- handling sums position-dependently needs a position-indexed representation.

class Netlist (p :: Poly) where
  -- | Extract the position and pin assignment from a polynomial value.
  toNet :: Eval p x -> (Pos p, Dir p -> x)

  -- | Build a polynomial value from a position and pin assignment.
  fromNet :: Pos p -> (Dir p -> x) -> Eval p x

instance Netlist 'Y where
  toNet :: forall x. Eval 'Y x -> (Pos 'Y, Dir 'Y -> x)
toNet (EY x
x) = ((), \() -> x
x)
  fromNet :: forall x. Pos 'Y -> (Dir 'Y -> x) -> Eval 'Y x
fromNet () Dir 'Y -> x
k = x -> Eval 'Y x
forall x. x -> Eval 'Y x
EY (Dir 'Y -> x
k ())

instance Netlist ('Const a) where
  toNet :: forall x.
Eval ('Const a) x -> (Pos ('Const a), Dir ('Const a) -> x)
toNet (EK c
c) = (c
Pos ('Const a)
c, Void -> x
Dir ('Const a) -> x
forall a. Void -> a
absurd)
  fromNet :: forall x.
Pos ('Const a) -> (Dir ('Const a) -> x) -> Eval ('Const a) x
fromNet Pos ('Const a)
c Dir ('Const a) -> x
_ = a -> Eval ('Const a) x
forall p x. p -> Eval ('Const p) x
EK a
Pos ('Const a)
c

instance Netlist ('Exp a) where
  toNet :: forall x. Eval ('Exp a) x -> (Pos ('Exp a), Dir ('Exp a) -> x)
toNet (EE a -> x
f) = ((), a -> x
Dir ('Exp a) -> x
f)
  fromNet :: forall x. Pos ('Exp a) -> (Dir ('Exp a) -> x) -> Eval ('Exp a) x
fromNet () = (a -> x) -> Eval ('Exp a) x
(Dir ('Exp a) -> x) -> Eval ('Exp a) x
forall p x. (p -> x) -> Eval ('Exp p) x
EE

instance (Netlist p, Netlist q) => Netlist ('Prod p q) where
  toNet :: forall x.
Eval ('Prod p q) x -> (Pos ('Prod p q), Dir ('Prod p q) -> x)
toNet (EP (Eval p x
u, Eval q x
v)) =
    let (Pos p
i, Dir p -> x
f) = Eval p x -> (Pos p, Dir p -> x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p x
u
        (Pos q
j, Dir q -> x
g) = Eval q x -> (Pos q, Dir q -> x)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval q x
v
     in ((Pos p
Pos p
i, Pos q
Pos q
j), (Dir p -> x) -> (Dir q -> x) -> Either (Dir p) (Dir q) -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Dir p -> x
Dir p -> x
f Dir q -> x
Dir q -> x
g)
  fromNet :: forall x.
Pos ('Prod p q) -> (Dir ('Prod p q) -> x) -> Eval ('Prod p q) x
fromNet (Pos p
i, Pos q
j) Dir ('Prod p q) -> x
k = (Eval p x, Eval q x) -> Eval ('Prod p q) x
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos p
i (Either (Dir p) (Dir q) -> x
Dir ('Prod p q) -> x
k (Either (Dir p) (Dir q) -> x)
-> (Dir p -> Either (Dir p) (Dir q)) -> Dir p -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Dir p -> Either (Dir p) (Dir q)
forall a b. a -> Either a b
Left), Pos q -> (Dir q -> x) -> Eval q x
forall x. Pos q -> (Dir q -> x) -> Eval q x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos q
j (Either (Dir p) (Dir q) -> x
Dir ('Prod p q) -> x
k (Either (Dir p) (Dir q) -> x)
-> (Dir q -> Either (Dir p) (Dir q)) -> Dir q -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Dir q -> Either (Dir p) (Dir q)
forall a b. b -> Either a b
Right))

instance Netlist ('Tensor p q) where
  toNet :: forall x.
Eval ('Tensor p q) x -> (Pos ('Tensor p q), Dir ('Tensor p q) -> x)
toNet (ET (Pos p, Pos q)
ij (Dir p, Dir q) -> x
f) = ((Pos p, Pos q)
Pos ('Tensor p q)
ij, (Dir p, Dir q) -> x
Dir ('Tensor p q) -> x
f)
  fromNet :: forall x.
Pos ('Tensor p q)
-> (Dir ('Tensor p q) -> x) -> Eval ('Tensor p q) x
fromNet = (Pos p, Pos q) -> ((Dir p, Dir q) -> x) -> Eval ('Tensor p q) x
Pos ('Tensor p q)
-> (Dir ('Tensor p q) -> x) -> Eval ('Tensor p q) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET

instance Netlist ('Comp p q) where
  toNet :: forall x.
Eval ('Comp p q) x -> (Pos ('Comp p q), Dir ('Comp p q) -> x)
toNet (EC (Pos p, Dir p -> Pos q)
i (Dir p, Dir q) -> x
k) = ((Pos p, Dir p -> Pos q)
Pos ('Comp p q)
i, (Dir p, Dir q) -> x
Dir ('Comp p q) -> x
k)
  fromNet :: forall x.
Pos ('Comp p q) -> (Dir ('Comp p q) -> x) -> Eval ('Comp p q) x
fromNet = (Pos p, Dir p -> Pos q)
-> ((Dir p, Dir q) -> x) -> Eval ('Comp p q) x
Pos ('Comp p q) -> (Dir ('Comp p q) -> x) -> Eval ('Comp p q) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC

-- | Reassemble a value after taking it apart. This is the executable form
-- of the round-trip law @'fromNet' ('toNet' v) ≡ v@.
netRoundTrip :: (Netlist p) => Eval p x -> Eval p x
netRoundTrip :: forall (p :: Poly) x. Netlist p => Eval p x -> Eval p x
netRoundTrip Eval p x
v = (Pos p -> (Dir p -> x) -> Eval p x)
-> (Pos p, Dir p -> x) -> Eval p x
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet (Eval p x -> (Pos p, Dir p -> x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p x
v)

-- | Left unitor for the Dirichlet tensor: @Y ⊗ p ≅ p@.
--
-- The @Y@ factor is degenerate; collapse via 'fromNet' on the other factor.
tensorUnitorL :: (Netlist p) => Eval ('Tensor 'Y p) x -> Eval p x
tensorUnitorL :: forall (p :: Poly) x.
Netlist p =>
Eval ('Tensor 'Y p) x -> Eval p x
tensorUnitorL (ET ((), Pos q
i) (Dir p, Dir q) -> x
f) = Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos p
Pos q
i (\Dir p
dp -> (Dir p, Dir q) -> x
f ((), Dir p
Dir q
dp))

-- | Inverse left unitor: @p -> Y ⊗ p@.
tensorUnitorL' :: (Netlist p) => Eval p x -> Eval ('Tensor 'Y p) x
tensorUnitorL' :: forall (p :: Poly) x.
Netlist p =>
Eval p x -> Eval ('Tensor 'Y p) x
tensorUnitorL' Eval p x
v =
  let (Pos p
i, Dir p -> x
k) = Eval p x -> (Pos p, Dir p -> x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p x
v
   in (Pos 'Y, Pos p) -> ((Dir 'Y, Dir p) -> x) -> Eval ('Tensor 'Y p) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET ((), Pos p
i) (\((), Dir p
dp) -> Dir p -> x
k Dir p
dp)

-- | Right unitor for the Dirichlet tensor: @p ⊗ Y ≅ p@.
tensorUnitorR :: (Netlist p) => Eval ('Tensor p 'Y) x -> Eval p x
tensorUnitorR :: forall (p :: Poly) x.
Netlist p =>
Eval ('Tensor p 'Y) x -> Eval p x
tensorUnitorR (ET (Pos p
i, ()) (Dir p, Dir q) -> x
f) = Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos p
Pos p
i (\Dir p
dp -> (Dir p, Dir q) -> x
f (Dir p
Dir p
dp, ()))

-- | Inverse right unitor: @p -> p ⊗ Y@.
tensorUnitorR' :: (Netlist p) => Eval p x -> Eval ('Tensor p 'Y) x
tensorUnitorR' :: forall (p :: Poly) x.
Netlist p =>
Eval p x -> Eval ('Tensor p 'Y) x
tensorUnitorR' Eval p x
v =
  let (Pos p
i, Dir p -> x
k) = Eval p x -> (Pos p, Dir p -> x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p x
v
   in (Pos p, Pos 'Y) -> ((Dir p, Dir 'Y) -> x) -> Eval ('Tensor p 'Y) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET (Pos p
i, ()) (\(Dir p
dp, ()) -> Dir p -> x
k Dir p
dp)

-- | Read the bundle map off a 'Morphism' at a chosen position.
--
-- Instantiating the output as @'Dir' p@ turns an opaque morphism into a
-- forward position plus a backward direction map — the crux that makes
-- 'parT' a few lines.
morphAt :: (Netlist p, Netlist p') => Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt :: forall (p :: Poly) (p' :: Poly).
(Netlist p, Netlist p') =>
Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt Morphism p p'
m Pos p
i =
  let (Pos p'
i', Dir p' -> Dir p
k) = Eval p' (Dir p) -> (Pos p', Dir p' -> Dir p)
forall x. Eval p' x -> (Pos p', Dir p' -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet (Morphism p p' -> forall x. Eval p x -> Eval p' x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p p'
m (Pos p -> (Dir p -> Dir p) -> Eval p (Dir p)
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos p
i Dir p -> Dir p
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id))
   in (Pos p'
i', Dir p' -> Dir p
k)

-- | Functorial action of the Dirichlet tensor on 'Netlist' factors.
--
-- Map each tensor factor through its morphism independently; backward
-- directions thread through both pullback maps.
parT ::
  (Netlist p, Netlist q, Netlist p', Netlist q') =>
  Morphism p p' ->
  Morphism q q' ->
  Eval ('Tensor p q) x ->
  Eval ('Tensor p' q') x
parT :: forall (p :: Poly) (q :: Poly) (p' :: Poly) (q' :: Poly) x.
(Netlist p, Netlist q, Netlist p', Netlist q') =>
Morphism p p'
-> Morphism q q' -> Eval ('Tensor p q) x -> Eval ('Tensor p' q') x
parT Morphism p p'
m Morphism q q'
n (ET (Pos p
i, Pos q
j) (Dir p, Dir q) -> x
f) =
  let (Pos p'
i', Dir p' -> Dir p
pullM) = Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
forall (p :: Poly) (p' :: Poly).
(Netlist p, Netlist p') =>
Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt Morphism p p'
m Pos p
Pos p
i
      (Pos q'
j', Dir q' -> Dir q
pullN) = Morphism q q' -> Pos q -> (Pos q', Dir q' -> Dir q)
forall (p :: Poly) (p' :: Poly).
(Netlist p, Netlist p') =>
Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt Morphism q q'
n Pos q
Pos q
j
   in (Pos p', Pos q')
-> ((Dir p', Dir q') -> x) -> Eval ('Tensor p' q') x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET (Pos p'
i', Pos q'
j') ((Dir p, Dir q) -> x
(Dir p, Dir q) -> x
f ((Dir p, Dir q) -> x)
-> ((Dir p', Dir q') -> (Dir p, Dir q)) -> (Dir p', Dir q') -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (Dir p' -> Dir p)
-> (Dir q' -> Dir q) -> (Dir p', Dir q') -> (Dir p, Dir q)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Dir p' -> Dir p
pullM Dir q' -> Dir q
pullN)

-- | Composition-product view of a nested evaluation @'Eval' p ('Eval' q x)@.
--
-- Correctness iso (right): @'Eval' ('Comp' p q) x ≅ 'Eval' p ('Eval' q x)@.
nestedToComp :: (Netlist p, Netlist q) => Eval p (Eval q x) -> Eval ('Comp p q) x
nestedToComp :: forall (p :: Poly) (q :: Poly) x.
(Netlist p, Netlist q) =>
Eval p (Eval q x) -> Eval ('Comp p q) x
nestedToComp Eval p (Eval q x)
v =
  let (Pos p
i, Dir p -> Eval q x
g) = Eval p (Eval q x) -> (Pos p, Dir p -> Eval q x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p (Eval q x)
v
   in (Pos p, Dir p -> Pos q)
-> ((Dir p, Dir q) -> x) -> Eval ('Comp p q) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC (Pos p
i, (Pos q, Dir q -> x) -> Pos q
forall a b. (a, b) -> a
fst ((Pos q, Dir q -> x) -> Pos q)
-> (Eval q x -> (Pos q, Dir q -> x)) -> Eval q x -> Pos q
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Eval q x -> (Pos q, Dir q -> x)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet (Eval q x -> Pos q) -> (Dir p -> Eval q x) -> Dir p -> Pos q
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Dir p -> Eval q x
g) (\(Dir p
dp, Dir q
dq) -> (Pos q, Dir q -> x) -> Dir q -> x
forall a b. (a, b) -> b
snd (Eval q x -> (Pos q, Dir q -> x)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet (Dir p -> Eval q x
g Dir p
dp)) Dir q
dq)

-- | Nested evaluation from a composition-product value.
--
-- Correctness iso (left): inverse of 'nestedToComp'.
compToNested :: (Netlist p, Netlist q) => Eval ('Comp p q) x -> Eval p (Eval q x)
compToNested :: forall (p :: Poly) (q :: Poly) x.
(Netlist p, Netlist q) =>
Eval ('Comp p q) x -> Eval p (Eval q x)
compToNested (EC (Pos p
i, Dir p -> Pos q
hang) (Dir p, Dir q) -> x
k) =
  Pos p -> (Dir p -> Eval q x) -> Eval p (Eval q x)
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos p
Pos p
i (\Dir p
dp -> Pos q -> (Dir q -> x) -> Eval q x
forall x. Pos q -> (Dir q -> x) -> Eval q x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet (Dir p -> Pos q
hang Dir p
Dir p
dp) (\Dir q
dq -> (Dir p, Dir q) -> x
k (Dir p
Dir p
dp, Dir q
Dir q
dq)))

-- | Left unitor for the composition product: @Y ◁ p -> p@.
compUnitorL :: (Netlist p) => Eval ('Comp 'Y p) x -> Eval p x
compUnitorL :: forall (p :: Poly) x. Netlist p => Eval ('Comp 'Y p) x -> Eval p x
compUnitorL (EC ((), Dir p -> Pos q
hang) (Dir p, Dir q) -> x
k) =
  Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet (Dir p -> Pos q
hang ()) (\Dir p
dp -> (Dir p, Dir q) -> x
k ((), Dir p
Dir q
dp))

-- | Inverse left unitor for the composition product: @p -> Y ◁ p@.
compUnitorL' :: (Netlist p) => Eval p x -> Eval ('Comp 'Y p) x
compUnitorL' :: forall (p :: Poly) x. Netlist p => Eval p x -> Eval ('Comp 'Y p) x
compUnitorL' Eval p x
v =
  let (Pos p
i, Dir p -> x
k) = Eval p x -> (Pos p, Dir p -> x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p x
v
   in (Pos 'Y, Dir 'Y -> Pos p)
-> ((Dir 'Y, Dir p) -> x) -> Eval ('Comp 'Y p) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC ((), Pos p -> () -> Pos p
forall a b. a -> b -> a
const Pos p
i) (\((), Dir p
dp) -> Dir p -> x
k Dir p
dp)

-- | Right unitor for the composition product: @p ◁ Y -> p@.
compUnitorR :: (Netlist p) => Eval ('Comp p 'Y) x -> Eval p x
compUnitorR :: forall (p :: Poly) x. Netlist p => Eval ('Comp p 'Y) x -> Eval p x
compUnitorR (EC (Pos p
i, Dir p -> Pos q
_) (Dir p, Dir q) -> x
k) =
  Pos p -> (Dir p -> x) -> Eval p x
forall x. Pos p -> (Dir p -> x) -> Eval p x
forall (p :: Poly) x.
Netlist p =>
Pos p -> (Dir p -> x) -> Eval p x
fromNet Pos p
Pos p
i (\Dir p
dp -> (Dir p, Dir q) -> x
k (Dir p
Dir p
dp, ()))

-- | Inverse right unitor for the composition product: @p -> p ◁ Y@.
compUnitorR' :: (Netlist p) => Eval p x -> Eval ('Comp p 'Y) x
compUnitorR' :: forall (p :: Poly) x. Netlist p => Eval p x -> Eval ('Comp p 'Y) x
compUnitorR' Eval p x
v =
  let (Pos p
i, Dir p -> x
k) = Eval p x -> (Pos p, Dir p -> x)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p x
v
   in (Pos p, Dir p -> Pos 'Y)
-> ((Dir p, Dir 'Y) -> x) -> Eval ('Comp p 'Y) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC (Pos p
i, () -> Dir p -> ()
forall a b. a -> b -> a
const ()) (\(Dir p
dp, ()) -> Dir p -> x
k Dir p
dp)

-- | Left associator for the composition product:
-- @((p ◁ q) ◁ r) -> (p ◁ (q ◁ r))@.
compAssocL :: Eval ('Comp ('Comp p q) r) x -> Eval ('Comp p ('Comp q r)) x
compAssocL :: forall (p :: Poly) (q :: Poly) (r :: Poly) x.
Eval ('Comp ('Comp p q) r) x -> Eval ('Comp p ('Comp q r)) x
compAssocL (EC ((Pos p
i, Dir p -> Pos q
f), Dir p -> Pos q
g) (Dir p, Dir q) -> x
k) =
  (Pos p, Dir p -> Pos ('Comp q r))
-> ((Dir p, Dir ('Comp q r)) -> x) -> Eval ('Comp p ('Comp q r)) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC
    ( Pos p
i,
      \Dir p
dp ->
        let j :: Pos q
j = Dir p -> Pos q
f Dir p
dp
            h :: Dir q -> Pos q
h Dir q
dq = Dir p -> Pos q
g (Dir p
dp, Dir q
dq)
         in (Pos q
j, Dir q -> Pos r
Dir q -> Pos q
h)
    )
    (\(Dir p
dp, (Dir q
dq, Dir r
dr)) -> (Dir p, Dir q) -> x
k ((Dir p
dp, Dir q
dq), Dir r
Dir q
dr))

-- | Right associator for the composition product.
compAssocR :: Eval ('Comp p ('Comp q r)) x -> Eval ('Comp ('Comp p q) r) x
compAssocR :: forall (p :: Poly) (q :: Poly) (r :: Poly) x.
Eval ('Comp p ('Comp q r)) x -> Eval ('Comp ('Comp p q) r) x
compAssocR (EC (Pos p
i, Dir p -> Pos q
h) (Dir p, Dir q) -> x
k) =
  let f :: Dir p -> Pos q
f = (Pos q, Dir q -> Pos r) -> Pos q
forall a b. (a, b) -> a
fst ((Pos q, Dir q -> Pos r) -> Pos q)
-> (Dir p -> (Pos q, Dir q -> Pos r)) -> Dir p -> Pos q
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Dir p -> (Pos q, Dir q -> Pos r)
Dir p -> Pos q
h
      g :: (Dir p, Dir q) -> Pos r
g (Dir p
dp, Dir q
dq) = (Pos q, Dir q -> Pos r) -> Dir q -> Pos r
forall a b. (a, b) -> b
snd (Dir p -> Pos q
h Dir p
Dir p
dp) Dir q
dq
   in (Pos ('Comp p q), Dir ('Comp p q) -> Pos r)
-> ((Dir ('Comp p q), Dir r) -> x) -> Eval ('Comp ('Comp p q) r) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC ((Pos p
Pos p
i, Dir p -> Pos q
f), (Dir p, Dir q) -> Pos r
Dir ('Comp p q) -> Pos r
g) (\((Dir p
dp, Dir q
dq), Dir r
dr) -> (Dir p, Dir q) -> x
k (Dir p
Dir p
dp, (Dir q
dq, Dir r
dr)))

-- | Functorial action of the composition product on monomial morphisms.
compT ::
  Morphism (Mono da a) (Mono db b) ->
  Morphism (Mono dc c) (Mono dd d) ->
  Eval ('Comp (Mono da a) (Mono dc c)) x ->
  Eval ('Comp (Mono db b) (Mono dd d)) x
compT :: forall da a db b dc c dd d x.
Morphism (Mono da a) (Mono db b)
-> Morphism (Mono dc c) (Mono dd d)
-> Eval ('Comp (Mono da a) (Mono dc c)) x
-> Eval ('Comp (Mono db b) (Mono dd d)) x
compT Morphism (Mono da a) (Mono db b)
f Morphism (Mono dc c) (Mono dd d)
g (EC (Pos p
aPos, Dir p -> Pos q
hang) (Dir p, Dir q) -> x
k) =
  let ((b
bPos, ()), Dir (Mono db b) -> Dir (Mono da a)
fBw) = Morphism (Mono da a) (Mono db b)
-> Pos (Mono da a)
-> (Pos (Mono db b), Dir (Mono db b) -> Dir (Mono da a))
forall (p :: Poly) (p' :: Poly).
(Netlist p, Netlist p') =>
Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt Morphism (Mono da a) (Mono db b)
f Pos p
Pos (Mono da a)
aPos
      newHang :: Either Void db -> Pos (Mono dd d)
newHang Either Void db
db =
        let da :: Dir (Mono da a)
da = Dir (Mono db b) -> Dir (Mono da a)
fBw Either Void db
Dir (Mono db b)
db
            cPos :: Pos q
cPos = Dir p -> Pos q
hang Dir p
Dir (Mono da a)
da
            (Pos (Mono dd d)
dPos, Dir (Mono dd d) -> Dir (Mono dc c)
_) = Morphism (Mono dc c) (Mono dd d)
-> Pos (Mono dc c)
-> (Pos (Mono dd d), Dir (Mono dd d) -> Dir (Mono dc c))
forall (p :: Poly) (p' :: Poly).
(Netlist p, Netlist p') =>
Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt Morphism (Mono dc c) (Mono dd d)
g Pos q
Pos (Mono dc c)
cPos
         in Pos (Mono dd d)
dPos
      newK :: (Either Void db, Either Void dd) -> x
newK (Either Void db
db, Either Void dd
dd) =
        let da :: Dir (Mono da a)
da = Dir (Mono db b) -> Dir (Mono da a)
fBw Either Void db
Dir (Mono db b)
db
            cPos :: Pos q
cPos = Dir p -> Pos q
hang Dir p
Dir (Mono da a)
da
            (Pos (Mono dd d)
_, Dir (Mono dd d) -> Dir (Mono dc c)
gBw) = Morphism (Mono dc c) (Mono dd d)
-> Pos (Mono dc c)
-> (Pos (Mono dd d), Dir (Mono dd d) -> Dir (Mono dc c))
forall (p :: Poly) (p' :: Poly).
(Netlist p, Netlist p') =>
Morphism p p' -> Pos p -> (Pos p', Dir p' -> Dir p)
morphAt Morphism (Mono dc c) (Mono dd d)
g Pos q
Pos (Mono dc c)
cPos
            dc :: Dir (Mono dc c)
dc = Dir (Mono dd d) -> Dir (Mono dc c)
gBw Either Void dd
Dir (Mono dd d)
dd
         in (Dir p, Dir q) -> x
k (Dir p
Dir (Mono da a)
da, Dir q
Dir (Mono dc c)
dc)
   in (Pos (Mono db b), Dir (Mono db b) -> Pos (Mono dd d))
-> ((Dir (Mono db b), Dir (Mono dd d)) -> x)
-> Eval ('Comp (Mono db b) (Mono dd d)) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Dir p -> Pos b)
-> ((Dir p, Dir b) -> x) -> Eval ('Comp p b) x
EC ((b
bPos, ()), Either Void db -> Pos (Mono dd d)
Dir (Mono db b) -> Pos (Mono dd d)
newHang) (Either Void db, Either Void dd) -> x
(Dir (Mono db b), Dir (Mono dd d)) -> x
newK

-- | Pair two polynomial values into a Dirichlet tensor (@p ⊗ q@).
--
-- Each factor contributes its position and pin assignment; the result is
-- one joint assignment over the product of direction sets.
tensorEval :: (Netlist p, Netlist q) => Eval p a -> Eval q b -> Eval (Tensor p q) (a, b)
tensorEval :: forall (p :: Poly) (q :: Poly) a b.
(Netlist p, Netlist q) =>
Eval p a -> Eval q b -> Eval ('Tensor p q) (a, b)
tensorEval Eval p a
v Eval q b
w =
  let (Pos p
i, Dir p -> a
fv) = Eval p a -> (Pos p, Dir p -> a)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval p a
v
      (Pos q
j, Dir q -> b
fw) = Eval q b -> (Pos q, Dir q -> b)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x. Netlist p => Eval p x -> (Pos p, Dir p -> x)
toNet Eval q b
w
   in (Pos p, Pos q)
-> ((Dir p, Dir q) -> (a, b)) -> Eval ('Tensor p q) (a, b)
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET (Pos p
i, Pos q
j) ((Dir p -> a) -> (Dir q -> b) -> (Dir p, Dir q) -> (a, b)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Dir p -> a
fv Dir q -> b
fw)

-- $netlist-roundtrip
--
-- Round trips hold for the structural instances. The witnesses below are
-- chosen so that a placeholder 'fromNet'/'toNet' that ignores its input
-- would fail: they use non-identity pin assignments and non-unit direction
-- sets.
--
-- 'Y': the pin assignment is nondegenerate because it must return the stored
-- value.
--
-- >>> let yv = EY 'a' :: Eval 'Y Char
-- >>> case netRoundTrip yv of EY c -> c
-- 'a'
--
-- 'Const': the direction set is 'Void', so the assignment is unique.
--
-- >>> let cv = EK True :: Eval ('Const Bool) Bool
-- >>> case netRoundTrip cv of EK b -> b
-- True
--
-- 'Exp': round-trip holds pointwise on the direction set.
--
-- >>> let ev = EE (\case 'a' -> 1; 'b' -> 2; _ -> 3) :: Eval ('Exp Char) Int
-- >>> case netRoundTrip ev of EE f -> (f 'a', f 'b', f 'c')
-- (1,2,3)
--
-- 'Prod': directions split over 'Either'; the witness uses different
-- behaviour on each side. Both factors here are 'Exp Char' so a mutant that
-- sends both sides through 'Left' still compiles but produces the wrong value
-- on the right.
--
-- >>> let pv = EP (EE (\c -> c : "!"), EE (\c -> c : "?")) :: Eval ('Prod ('Exp Char) ('Exp Char)) String
-- >>> case netRoundTrip pv of EP (EE f, EE g) -> (f 'x', g 'y')
-- ("x!","y?")
--
-- 'Tensor': the constructor already /is/ netlist form, but the witness
-- still exercises the split product of directions.
--
-- >>> let tv = ET ((), ()) (\(d1, d2) -> d1 ++ d2) :: Eval ('Tensor ('Exp String) ('Exp String)) String
-- >>> case netRoundTrip tv of ET ((), ()) f -> f ("hello ", "world")
-- "hello world"
--
-- The position-round-trip law @toNet ('fromNet' i k) == (i, k)@ also holds
-- pointwise. For 'Prod' this is where a broken split would show up.
--
-- >>> let (i, k) = toNet (fromNet ((), ()) (\case Left c -> c : "!"; Right b -> if b then "yes" else "no") :: Eval ('Prod ('Exp Char) ('Exp Bool)) String)
-- >>> (i, k (Left 'x'), k (Right False))
-- (((),()),"x!","no")
--
-- Left unitor: @Y ⊗ Mono@ collapses to @Mono@ and back.  Pin assignment
-- transforms (@dn -> show dn ++ "!"@) — a stub that ignores @f@ fails.
--
-- >>> let yt = ET ((), (5, ())) (\((), Right dn) -> show dn ++ "!") :: Eval ('Tensor 'Y (Mono Int Int)) String
-- >>> case tensorUnitorL yt of EP (EK n, EE f) -> (n, f 7, f 42)
-- (5,"7!","42!")
--
-- >>> let mono = EP (EK 5, EE (\dn -> show dn ++ "!")) :: Eval (Mono Int Int) String
-- >>> case tensorUnitorL' mono of ET ((), (n, ())) f -> (n, f ((), Right 7))
-- (5,"7!")
--
-- >>> case tensorUnitorL (tensorUnitorL' mono) of EP (EK n, EE f) -> (n, f 3)
-- (5,"3!")
--
-- Right unitor: position pair @(i, ())@ not @(() , i)@.
--
-- >>> let ty = ET ((5, ()), ()) (\(Right dn, ()) -> dn + 10) :: Eval ('Tensor (Mono Int Int) 'Y) Int
-- >>> case tensorUnitorR ty of EP (EK n, EE f) -> (n, f 3, f 7)
-- (5,13,17)
--
-- >>> let monoInt = EP (EK 5, EE (\dn -> dn + 1)) :: Eval (Mono Int Int) Int
-- >>> case tensorUnitorR (tensorUnitorR' monoInt) of EP (EK n, EE f) -> (n, f 3)
-- (5,4)

-- | A morphism @p -> q@ in Poly, encoded as a natural transformation
-- between the evaluated functors.
--
-- By the Yoneda / sigma universal property, this is equivalent to a
-- bundle map: a function on positions together with a contravariant
-- family of functions on directions.
--
-- 'Konst' and 'Depend' extend the original Poly sketch so that backward
-- maps can depend on the current position, giving point-dependent lenses.
data Morphism (p :: Poly) (q :: Poly) where
  -- | Identity morphism.
  Id :: Morphism p p
  -- | Global element: a point of @q@ as a morphism @Y -> q@.
  --
  -- By the Yoneda lemma, @Poly(Y, q) ≅ q(1) ≅ Eval q ()@.
  Point :: Eval q () -> Morphism 'Y q
  -- | Covariant embedding of a plain function into constants.
  ConstMap :: (a -> b) -> Morphism ('Const a) ('Const b)
  -- | Contravariant embedding of a plain function into exponentials.
  ExpMap :: (a -> b) -> Morphism ('Exp b) ('Exp a)
  -- | Sequential composition.
  Compose :: Morphism q r -> Morphism p q -> Morphism p r
  -- | Parallel composition (cartesian product of morphisms).
  Par :: Morphism p p' -> Morphism q q' -> Morphism ('Prod p q) ('Prod p' q')
  -- | Coproduct injections.
  Inl :: Morphism p ('Sum p q)
  Inr :: Morphism q ('Sum p q)
  -- | Coproduct case analysis.
  Case :: Morphism p r -> Morphism q r -> Morphism ('Sum p q) r
  -- | Product projections.
  Fst :: Morphism ('Prod p q) p
  Snd :: Morphism ('Prod p q) q
  -- | Product pairing.
  Pair :: Morphism r p -> Morphism r q -> Morphism r ('Prod p q)
  -- | Global element (constant introduction).
  Konst :: b -> Morphism p ('Const b)
  -- | Copower universal property: a @Const a@-indexed family of morphisms.
  Depend :: (a -> Morphism p q) -> Morphism ('Prod ('Const a) p) q
  -- | Left associator for the Dirichlet tensor:
  -- @((p ⊗ q) ⊗ r) -> (p ⊗ (q ⊗ r))@.
  TensorAssocL :: Morphism ('Tensor ('Tensor p q) r) ('Tensor p ('Tensor q r))
  -- | Right associator for the Dirichlet tensor.
  TensorAssocR :: Morphism ('Tensor p ('Tensor q r)) ('Tensor ('Tensor p q) r)
  -- | Symmetry/braiding for the Dirichlet tensor: @p ⊗ q -> q ⊗ p@.
  TensorBraid :: Morphism ('Tensor p q) ('Tensor q p)
  -- | Functorial action of the Dirichlet tensor on monomial morphisms:
  -- @f ⊗ g : (a·y^{da}) ⊗ (c·y^{dc}) -> (b·y^{db}) ⊗ (d·y^{dd})@.
  --
  -- Restricted to monomials because the current 'Dir' family cannot express
  -- position-dependent direction sets (in particular, 'Sum' has no 'Dir' row).
  ParT ::
    Morphism (Mono da a) (Mono db b) ->
    Morphism (Mono dc c) (Mono dd d) ->
    Morphism ('Tensor (Mono da a) (Mono dc c)) ('Tensor (Mono db b) (Mono dd d))
  -- | Left unitor for the composition product: @Y ◁ p ≅ p@.
  CompUnitL :: (Netlist p) => Morphism ('Comp 'Y p) p
  -- | Inverse left unitor for the composition product.
  CompUnitL' :: (Netlist p) => Morphism p ('Comp 'Y p)
  -- | Right unitor for the composition product: @p ◁ Y ≅ p@.
  CompUnitR :: (Netlist p) => Morphism ('Comp p 'Y) p
  -- | Inverse right unitor for the composition product.
  CompUnitR' :: (Netlist p) => Morphism p ('Comp p 'Y)
  -- | Left associator for the composition product:
  -- @((p ◁ q) ◁ r) -> (p ◁ (q ◁ r))@.
  CompAssocL :: Morphism ('Comp ('Comp p q) r) ('Comp p ('Comp q r))
  -- | Right associator for the composition product.
  CompAssocR :: Morphism ('Comp p ('Comp q r)) ('Comp ('Comp p q) r)
  -- | Functorial action of the composition product on monomial morphisms:
  -- @f ◁ g : (a·y^{da}) ◁ (c·y^{dc}) -> (b·y^{db}) ◁ (d·y^{dd})@.
  --
  -- Restricted to monomials for the same reason as 'ParT'.
  CompT ::
    Morphism (Mono da a) (Mono db b) ->
    Morphism (Mono dc c) (Mono dd d) ->
    Morphism ('Comp (Mono da a) (Mono dc c)) ('Comp (Mono db b) (Mono dd d))
  -- | Prism: a co-lens that matches on a sum-like position.
  --
  -- Forward pass @match :: s -> Either a s@; backward pass on the matched
  -- branch is @build :: a -> s@.  On the unmatched branch the backward pass
  -- is the identity.  Directions are identified with positions, which is the
  -- natural reading for set-valued polynomials.
  Prism ::
    (s -> Either a s) ->
    (a -> s) ->
    Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))

instance Category Morphism where
  id :: forall (a :: Poly). Morphism a a
id = Morphism a a
forall (a :: Poly). Morphism a a
Id
  . :: forall (b :: Poly) (c :: Poly) (a :: Poly).
Morphism b c -> Morphism a b -> Morphism a c
(.) = Morphism b c -> Morphism a b -> Morphism a c
forall (b :: Poly) (c :: Poly) (a :: Poly).
Morphism b c -> Morphism a b -> Morphism a c
Compose

-- | Interpret a 'Morphism' as a natural transformation.
runMorphism :: Morphism p q -> (forall x. Eval p x -> Eval q x)
runMorphism :: forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism = \case
  Morphism p q
Id -> Eval p x -> Eval p x
Eval p x -> Eval q x
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  Point Eval q ()
u -> \(EY x
v) -> (() -> x) -> Eval q () -> Eval q x
forall a b. (a -> b) -> Eval q a -> Eval q b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (x -> () -> x
forall a b. a -> b -> a
const x
v) Eval q ()
u
  ConstMap a -> b
f -> \(EK c
a) -> b -> Eval ('Const b) x
forall p x. p -> Eval ('Const p) x
EK (a -> b
f a
c
a)
  ExpMap a -> b
f -> \(EE a -> x
g) -> (a -> x) -> Eval ('Exp a) x
forall p x. (p -> x) -> Eval ('Exp p) x
EE (b -> x
a -> x
g (b -> x) -> (a -> b) -> a -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> b
f)
  Compose Morphism q q
g Morphism p q
f -> Morphism q q -> forall x. Eval q x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism q q
g (Eval q x -> Eval q x)
-> (Eval p x -> Eval q x) -> Eval p x -> Eval q x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Morphism p q -> forall x. Eval p x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p q
f
  Par Morphism p p'
f Morphism q q'
g -> \(EP (Eval p x
a, Eval q x
b)) -> (Eval p' x, Eval q' x) -> Eval ('Prod p' q') x
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (Morphism p p' -> forall x. Eval p x -> Eval p' x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p p'
f Eval p x
Eval p x
a, Morphism q q' -> forall x. Eval q x -> Eval q' x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism q q'
g Eval q x
Eval q x
b)
  Morphism p q
Inl -> Either (Eval p x) (Eval q x) -> Eval ('Sum p q) x
forall (p :: Poly) x (b :: Poly).
Either (Eval p x) (Eval b x) -> Eval ('Sum p b) x
ES (Either (Eval p x) (Eval q x) -> Eval ('Sum p q) x)
-> (Eval p x -> Either (Eval p x) (Eval q x))
-> Eval p x
-> Eval ('Sum p q) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Eval p x -> Either (Eval p x) (Eval q x)
forall a b. a -> Either a b
Left
  Morphism p q
Inr -> Either (Eval p x) (Eval p x) -> Eval ('Sum p p) x
forall (p :: Poly) x (b :: Poly).
Either (Eval p x) (Eval b x) -> Eval ('Sum p b) x
ES (Either (Eval p x) (Eval p x) -> Eval ('Sum p p) x)
-> (Eval p x -> Either (Eval p x) (Eval p x))
-> Eval p x
-> Eval ('Sum p p) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Eval p x -> Either (Eval p x) (Eval p x)
forall a b. b -> Either a b
Right
  Case Morphism p q
f Morphism q q
g -> \case
    ES (Left Eval p x
a) -> Morphism p q -> forall x. Eval p x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p q
f Eval p x
Eval p x
a
    ES (Right Eval q x
b) -> Morphism q q -> forall x. Eval q x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism q q
g Eval q x
Eval q x
b
  Morphism p q
Fst -> \(EP (Eval p x
a, Eval q x
_)) -> Eval q x
Eval p x
a
  Morphism p q
Snd -> \(EP (Eval p x
_, Eval q x
b)) -> Eval q x
Eval q x
b
  Pair Morphism p p
f Morphism p q
g -> \Eval p x
r -> (Eval p x, Eval q x) -> Eval ('Prod p q) x
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (Morphism p p -> forall x. Eval p x -> Eval p x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p p
f Eval p x
r, Morphism p q -> forall x. Eval p x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p q
g Eval p x
r)
  Konst b
b -> \Eval p x
_ -> b -> Eval ('Const b) x
forall p x. p -> Eval ('Const p) x
EK b
b
  Depend a -> Morphism p q
k -> \(EP (EK c
a, Eval q x
p)) -> Morphism p q -> forall x. Eval p x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism (a -> Morphism p q
k a
c
a) Eval p x
Eval q x
p
  Morphism p q
TensorAssocL -> \(ET ((Pos p
pp, Pos q
pq), Pos q
pr) (Dir p, Dir q) -> x
f) ->
    (Pos p, Pos ('Tensor q r))
-> ((Dir p, Dir ('Tensor q r)) -> x)
-> Eval ('Tensor p ('Tensor q r)) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET (Pos p
pp, (Pos q
pq, Pos r
Pos q
pr)) (((Dir p, Dir q), Dir r) -> x
(Dir p, Dir q) -> x
f (((Dir p, Dir q), Dir r) -> x)
-> ((Dir p, (Dir q, Dir r)) -> ((Dir p, Dir q), Dir r))
-> (Dir p, (Dir q, Dir r))
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (\(Dir p
dp, (Dir q
dq, Dir r
dr)) -> ((Dir p
dp, Dir q
dq), Dir r
dr)))
  Morphism p q
TensorAssocR -> \(ET (Pos p
pp, (Pos q
pq, Pos r
pr)) (Dir p, Dir q) -> x
f) ->
    (Pos ('Tensor p q), Pos r)
-> ((Dir ('Tensor p q), Dir r) -> x)
-> Eval ('Tensor ('Tensor p q) r) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET ((Pos p
Pos p
pp, Pos q
pq), Pos r
pr) ((Dir p, (Dir q, Dir r)) -> x
(Dir p, Dir q) -> x
f ((Dir p, (Dir q, Dir r)) -> x)
-> (((Dir p, Dir q), Dir r) -> (Dir p, (Dir q, Dir r)))
-> ((Dir p, Dir q), Dir r)
-> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (\((Dir p
dp, Dir q
dq), Dir r
dr) -> (Dir p
dp, (Dir q
dq, Dir r
dr))))
  Morphism p q
TensorBraid -> \(ET (Pos p
pp, Pos q
pq) (Dir p, Dir q) -> x
f) ->
    (Pos q, Pos p) -> ((Dir q, Dir p) -> x) -> Eval ('Tensor q p) x
forall (p :: Poly) (b :: Poly) x.
(Pos p, Pos b) -> ((Dir p, Dir b) -> x) -> Eval ('Tensor p b) x
ET (Pos q
Pos q
pq, Pos p
Pos p
pp) ((Dir p, Dir q) -> x
(Dir p, Dir q) -> x
f ((Dir p, Dir q) -> x)
-> ((Dir q, Dir p) -> (Dir p, Dir q)) -> (Dir q, Dir p) -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. (\(Dir q
dq, Dir p
dp) -> (Dir p
dp, Dir q
dq)))
  ParT Morphism (Mono da a) (Mono db b)
m Morphism (Mono dc c) (Mono dd d)
n -> Morphism (Mono da a) (Mono db b)
-> Morphism (Mono dc c) (Mono dd d)
-> Eval ('Tensor (Mono da a) (Mono dc c)) x
-> Eval ('Tensor (Mono db b) (Mono dd d)) x
forall (p :: Poly) (q :: Poly) (p' :: Poly) (q' :: Poly) x.
(Netlist p, Netlist q, Netlist p', Netlist q') =>
Morphism p p'
-> Morphism q q' -> Eval ('Tensor p q) x -> Eval ('Tensor p' q') x
parT Morphism (Mono da a) (Mono db b)
m Morphism (Mono dc c) (Mono dd d)
n
  Morphism p q
CompUnitL -> Eval p x -> Eval q x
Eval ('Comp 'Y q) x -> Eval q x
forall (p :: Poly) x. Netlist p => Eval ('Comp 'Y p) x -> Eval p x
compUnitorL
  Morphism p q
CompUnitL' -> Eval p x -> Eval q x
Eval p x -> Eval ('Comp 'Y p) x
forall (p :: Poly) x. Netlist p => Eval p x -> Eval ('Comp 'Y p) x
compUnitorL'
  Morphism p q
CompUnitR -> Eval p x -> Eval q x
Eval ('Comp q 'Y) x -> Eval q x
forall (p :: Poly) x. Netlist p => Eval ('Comp p 'Y) x -> Eval p x
compUnitorR
  Morphism p q
CompUnitR' -> Eval p x -> Eval q x
Eval p x -> Eval ('Comp p 'Y) x
forall (p :: Poly) x. Netlist p => Eval p x -> Eval ('Comp p 'Y) x
compUnitorR'
  Morphism p q
CompAssocL -> Eval p x -> Eval q x
Eval ('Comp ('Comp p q) r) x -> Eval ('Comp p ('Comp q r)) x
forall (p :: Poly) (q :: Poly) (r :: Poly) x.
Eval ('Comp ('Comp p q) r) x -> Eval ('Comp p ('Comp q r)) x
compAssocL
  Morphism p q
CompAssocR -> Eval p x -> Eval q x
Eval ('Comp p ('Comp q r)) x -> Eval ('Comp ('Comp p q) r) x
forall (p :: Poly) (q :: Poly) (r :: Poly) x.
Eval ('Comp p ('Comp q r)) x -> Eval ('Comp ('Comp p q) r) x
compAssocR
  CompT Morphism (Mono da a) (Mono db b)
m Morphism (Mono dc c) (Mono dd d)
n -> Morphism (Mono da a) (Mono db b)
-> Morphism (Mono dc c) (Mono dd d)
-> Eval ('Comp (Mono da a) (Mono dc c)) x
-> Eval ('Comp (Mono db b) (Mono dd d)) x
forall da a db b dc c dd d x.
Morphism (Mono da a) (Mono db b)
-> Morphism (Mono dc c) (Mono dd d)
-> Eval ('Comp (Mono da a) (Mono dc c)) x
-> Eval ('Comp (Mono db b) (Mono dd d)) x
compT Morphism (Mono da a) (Mono db b)
m Morphism (Mono dc c) (Mono dd d)
n
  Prism s -> Either a s
match a -> s
build -> \case
    EP (EK c
s, EE a -> x
k) -> case s -> Either a s
match s
c
s of
      Left a
a -> Either (Eval (Mono a a) x) (Eval ('Prod ('Const s) ('Exp s)) x)
-> Eval ('Sum (Mono a a) ('Prod ('Const s) ('Exp s))) x
forall (p :: Poly) x (b :: Poly).
Either (Eval p x) (Eval b x) -> Eval ('Sum p b) x
ES (Eval (Mono a a) x
-> Either (Eval (Mono a a) x) (Eval ('Prod ('Const s) ('Exp s)) x)
forall a b. a -> Either a b
Left ((Eval ('Const a) x, Eval ('Exp a) x) -> Eval (Mono a a) x
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (a -> Eval ('Const a) x
forall p x. p -> Eval ('Const p) x
EK a
a, (a -> x) -> Eval ('Exp a) x
forall p x. (p -> x) -> Eval ('Exp p) x
EE (s -> x
a -> x
k (s -> x) -> (a -> s) -> a -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> s
build))))
      Right s
s' -> Either (Eval (Mono a a) x) (Eval ('Prod ('Const s) ('Exp a)) x)
-> Eval ('Sum (Mono a a) ('Prod ('Const s) ('Exp a))) x
forall (p :: Poly) x (b :: Poly).
Either (Eval p x) (Eval b x) -> Eval ('Sum p b) x
ES (Eval ('Prod ('Const s) ('Exp a)) x
-> Either (Eval (Mono a a) x) (Eval ('Prod ('Const s) ('Exp a)) x)
forall a b. b -> Either a b
Right ((Eval ('Const s) x, Eval ('Exp a) x)
-> Eval ('Prod ('Const s) ('Exp a)) x
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (s -> Eval ('Const s) x
forall p x. p -> Eval ('Const p) x
EK s
s', (a -> x) -> Eval ('Exp a) x
forall p x. (p -> x) -> Eval ('Exp p) x
EE a -> x
k)))

-- $dirichlet-tensor
--
-- The Dirichlet tensor @p ⊗ q@ pairs positions and multiplies directions.
-- A value is a position pair together with one function out of the product of
-- direction sets — not two separate functions.
--
-- >>> let ab = ET ((), ()) (\(a, b) -> a ++ b) :: Eval ('Tensor ('Exp String) ('Exp String)) String
-- >>> case ab of ET ((), ()) f -> f ("hello ", "world")
-- "hello world"
--
-- 'fmap' acts on the result of the combined direction function.
--
-- >>> let v = ET ((), ()) (\(a, b) -> a + b) :: Eval ('Tensor ('Exp Int) ('Exp Int)) Int
-- >>> case fmap (* 2) v of ET ((), ()) f -> f (3, 4)
-- 14
--
-- The braiding swaps both the position pair and the direction pair.
--
-- >>> case runMorphism TensorBraid ab of ET ((), ()) f -> f ("world", "hello ")
-- "hello world"
--
-- The associator reassociates both positions and directions.
--
-- >>> let abc = ET (((), ()), ()) (\((a, b), c) -> a ++ b ++ c) :: Eval ('Tensor ('Tensor ('Exp String) ('Exp String)) ('Exp String)) String
-- >>> case runMorphism TensorAssocL abc of ET ((), ((), ())) f -> f ("a", ("b", "c"))
-- "abc"
-- >>> case runMorphism TensorAssocR (runMorphism TensorAssocL abc) of ET (((), ()), ()) f -> f (("x", "y"), "z")
-- "xyz"
--
-- 'ParT' is the functorial action of tensor on monomials: map each factor
-- independently, backward directions thread through both.
--
-- The puts are deliberately non-identity: a test with identity puts would still
-- pass if ParT ignored the factor morphisms and threaded directions straight
-- through (the mutation-review catch).
--
-- >>> let m1 = lens show (\n dn -> n + dn) :: Morphism (Mono Int Int) (Mono Int String)
-- >>> let m2 = lens (\b -> if b then 1 else 0 :: Int) (\b db -> b && db) :: Morphism (Mono Bool Bool) (Mono Bool Int)
-- >>> let v = ET ((5, ()), (True, ())) (\(Right n, Right b) -> (n, b)) :: Eval ('Tensor (Mono Int Int) (Mono Bool Bool)) (Int, Bool)
-- >>> case runMorphism (ParT m1 m2) v of ET ((_, ()), (_, ())) f -> f (Right 3, Right True)
-- (8,True)
-- >>> case runMorphism (ParT m1 m2) v of ET ((_, ()), (_, ())) f -> f (Right 2, Right False)
-- (7,False)
--
-- 'parT' on non-monomial 'Netlist' factors ('Exp' morphisms via 'ExpMap').
-- Both pullbacks must fire; dropping either factor leaves the wrong sign.
--
-- >>> let v = ET ((), ()) (\(i, b) -> if b then i else -i) :: Eval ('Tensor ('Exp Int) ('Exp Bool)) Int
-- >>> let m = ExpMap (+ 10) :: Morphism ('Exp Int) ('Exp Int)
-- >>> let n = ExpMap not :: Morphism ('Exp Bool) ('Exp Bool)
-- >>> case parT m n v of ET ((), ()) g -> (g (3, True), g (0, False))
-- (-13,10)
--
-- >>> case parT m n v of ET ((), ()) g -> g (3, True)
-- -13

-- $composition-product
--
-- Correctness iso @'Eval' ('Comp' p q) x ≅ 'Eval' p ('Eval' q x)@.  The
-- @hang@ map must depend on the outer @p@-direction — a constant hang fails.
--
-- >>> let nested = EP (EK 5, EE (\dn -> EP (EK (show dn ++ "!"), EE (\c -> [c] ++ "?")))) :: Eval (Mono Int Int) (Eval (Mono Char String) String)
-- >>> case nestedToComp nested of EC ((n, ()), hang) k -> (n, fst (hang (Right 7)), k (Right 7, Right 'a'))
-- (5,"7!","a?")
--
-- >>> case compToNested (nestedToComp nested) of EP (EK n, EE f) -> case f 7 of EP (EK s, EE g) -> (n, s, g 'a')
-- (5,"7!","a?")
--
-- Two-step dynamics: @('Exp' Int ∘ 'Exp' Int)@ adds inputs along a path.
--
-- >>> let dyn = EE (\n -> EE (\m -> n + m)) :: Eval ('Exp Int) (Eval ('Exp Int) Int)
-- >>> case nestedToComp dyn of EC ((), hang) k -> k (10, 20)
-- 30
--
-- >>> case compToNested (nestedToComp dyn) of EE f -> case f 10 of EE g -> g 20
-- 30

-- $tensor-wiring
--
-- 'tensorEval' pairs factors; both pin maps must contribute (not just the
-- left factor).
--
-- >>> let va = EE (\x -> x ++ "x") :: Eval ('Exp String) String
-- >>> let vb = EE (\n -> n * 10) :: Eval ('Exp Int) Int
-- >>> case tensorEval va vb of ET ((), ()) f -> (f ("hi", 3), f ("", 0))
-- (("hix",30),("x",0))

-- | The monomial interface: @i@ directions (input), @o@ positions (output).
type Mono i o = 'Prod ('Const o) ('Exp i)

-- | The general point-dependent lens.
--
-- Forward pass @get :: a -> b@; backward pass @put :: a -> db -> da@
-- depends on the current position.
--
-- >>> let l = lens show (\n d -> n + d) :: Morphism (Mono Int Int) (Mono Int String)
-- >>> let (v, put) = applyLens l 40 in (v, put 2)
-- ("40",42)
lens :: (a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens :: forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens a -> b
f a -> db -> da
g = (a -> Morphism ('Exp da) (Mono db b))
-> Morphism ('Prod ('Const a) ('Exp da)) (Mono db b)
forall p (b :: Poly) (q :: Poly).
(p -> Morphism b q) -> Morphism ('Prod ('Const p) b) q
Depend (\a
a -> Morphism ('Exp da) ('Const b)
-> Morphism ('Exp da) ('Exp db) -> Morphism ('Exp da) (Mono db b)
forall (r :: Poly) (p :: Poly) (b :: Poly).
Morphism r p -> Morphism r b -> Morphism r ('Prod p b)
Pair (b -> Morphism ('Exp da) ('Const b)
forall p (p :: Poly). p -> Morphism p ('Const p)
Konst (a -> b
f a
a)) ((db -> da) -> Morphism ('Exp da) ('Exp db)
forall p b. (p -> b) -> Morphism ('Exp b) ('Exp p)
ExpMap (a -> db -> da
g a
a)))

-- | The position-independent dagger case.
--
-- Expressible without 'Konst' or 'Depend'.
--
-- >>> let d = dagger (+1) (subtract 1) :: Morphism (Mono Int Int) (Mono Int Int)
-- >>> let (v, put) = applyLens d 5 in (v, put 6)
-- (6,5)
dagger :: (a -> b) -> (db -> da) -> Morphism (Mono da a) (Mono db b)
dagger :: forall a b db da.
(a -> b) -> (db -> da) -> Morphism (Mono da a) (Mono db b)
dagger a -> b
f db -> da
g = Morphism (Mono da a) ('Const b)
-> Morphism (Mono da a) ('Exp db)
-> Morphism (Mono da a) ('Prod ('Const b) ('Exp db))
forall (r :: Poly) (p :: Poly) (b :: Poly).
Morphism r p -> Morphism r b -> Morphism r ('Prod p b)
Pair (Morphism ('Const a) ('Const b)
-> Morphism (Mono da a) ('Const a)
-> Morphism (Mono da a) ('Const b)
forall (b :: Poly) (c :: Poly) (a :: Poly).
Morphism b c -> Morphism a b -> Morphism a c
Compose ((a -> b) -> Morphism ('Const a) ('Const b)
forall p b. (p -> b) -> Morphism ('Const p) ('Const b)
ConstMap a -> b
f) Morphism (Mono da a) ('Const a)
forall (p :: Poly) (p :: Poly). Morphism ('Prod p p) p
Fst) (Morphism ('Exp da) ('Exp db)
-> Morphism (Mono da a) ('Exp da) -> Morphism (Mono da a) ('Exp db)
forall (b :: Poly) (c :: Poly) (a :: Poly).
Morphism b c -> Morphism a b -> Morphism a c
Compose ((db -> da) -> Morphism ('Exp da) ('Exp db)
forall p b. (p -> b) -> Morphism ('Exp b) ('Exp p)
ExpMap db -> da
g) Morphism (Mono da a) ('Exp da)
forall (p :: Poly) (q :: Poly). Morphism ('Prod p q) q
Snd)

-- | Apply a monomial morphism as a lens: @(get, put)@.
applyLens :: Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens :: forall da a db b.
Morphism (Mono da a) (Mono db b) -> a -> (b, db -> da)
applyLens Morphism (Mono da a) (Mono db b)
m a
a = case Morphism (Mono da a) (Mono db b)
-> forall x. Eval (Mono da a) x -> Eval (Mono db b) x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism (Mono da a) (Mono db b)
m ((Eval ('Const a) da, Eval ('Exp da) da) -> Eval (Mono da a) da
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (a -> Eval ('Const a) da
forall p x. p -> Eval ('Const p) x
EK a
a, (da -> da) -> Eval ('Exp da) da
forall p x. (p -> x) -> Eval ('Exp p) x
EE da -> da
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)) of
  EP (EK c
b, EE a -> da
g) -> (b
c
b, db -> da
a -> da
g)

-- | Prism: match on a sum-like source, build from the focused branch.
--
-- >>> let p = prism (\case Left n -> Left n; Right s -> Right (Right s)) Left :: Morphism (Mono (Either Int String) (Either Int String)) ('Sum (Mono Int Int) (Mono (Either Int String) (Either Int String)))
-- >>> case runMorphism p (EP (EK (Left 7), EE id)) of ES (Left (EP (EK n, EE k))) -> (n, k 1)
-- (7,Left 1)
prism ::
  (s -> Either a s) ->
  (a -> s) ->
  Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
prism :: forall s a.
(s -> Either a s)
-> (a -> s) -> Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
prism = (s -> Either a s)
-> (a -> s) -> Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
forall s a.
(s -> Either a s)
-> (a -> s) -> Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
Prism

-- | Extract the forward match of a prism.
prismMatch ::
  Morphism (Mono s s) ('Sum (Mono a a) (Mono s s)) ->
  s ->
  Either a s
prismMatch :: forall s a.
Morphism (Mono s s) ('Sum (Mono a a) (Mono s s)) -> s -> Either a s
prismMatch Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
p s
s = case Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
-> forall x.
   Eval (Mono s s) x -> Eval ('Sum (Mono a a) (Mono s s)) x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism (Mono s s) ('Sum (Mono a a) (Mono s s))
p ((Eval ('Const s) s, Eval ('Exp s) s) -> Eval (Mono s s) s
forall (p :: Poly) x (b :: Poly).
(Eval p x, Eval b x) -> Eval ('Prod p b) x
EP (s -> Eval ('Const s) s
forall p x. p -> Eval ('Const p) x
EK s
s, (s -> s) -> Eval ('Exp s) s
forall p x. (p -> x) -> Eval ('Exp p) x
EE s -> s
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id)) of
  ES (Left (EP (EK c
a, Eval q s
_))) -> a -> Either a s
forall a b. a -> Either a b
Left a
c
a
  ES (Right (EP (EK c
s', Eval q s
_))) -> s -> Either a s
forall a b. b -> Either a b
Right s
c
s'