Safe Haskell	None
Language	GHC2024

Circuit.PCA.Optic

Contents

Adapter to polynomial morphisms

Description

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

Synopsis

data Optic (mon :: k -> k1 -> Type) s u (a :: k1) (b :: k1) where
- Optic :: forall {k} {k1} s (mon :: k -> k1 -> Type) (m :: k) (a :: k1) (b :: k1) u. (s -> mon m a) -> (mon m b -> u) -> Optic mon s u a b
type Lens s t a b = Optic (,) s t a b
type OneShot s u a b = Optic (,) s u a b
fromClassical :: (s -> (a, b -> t)) -> Lens s t a b
toClassical :: Lens s t a b -> s -> (a, b -> t)
view :: Lens s s a a -> s -> a
set :: Lens s t a b -> b -> s -> t
over :: Lens s t a b -> (a -> b) -> s -> t
morphismAsLens :: Morphism (Mono s s) (Mono i o) -> Lens s s o i
lensAsMorphism :: Lens s s o i -> Morphism (Mono s s) (Mono i o)

Documentation

data Optic (mon :: k -> k1 -> Type) s u (a :: k1) (b :: k1) where Source #

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)

Constructors

Optic :: forall {k} {k1} s (mon :: k -> k1 -> Type) (m :: k) (a :: k1) (b :: k1) u. (s -> mon m a) -> (mon m b -> u) -> Optic mon s u a b

type Lens s t a b = Optic (,) s t a b Source #

Product-action optic = classical lens packing.

In classical notation the outer ends are named s, t rather than s, u.

type OneShot s u a b = Optic (,) s u a b Source #

One-shot product-residual optic.

This is the shape that a single state-changing morphism takes. It is not the same as System: a System has a fixed carrier and is iterable, whereas a OneShot morphism may change its outer state s -> u.

fromClassical :: (s -> (a, b -> t)) -> Lens s t a b Source #

Yoneda form s -> (a, b -> t) into existential residual form.

toClassical :: Lens s t a b -> s -> (a, b -> t) Source #

Existential residual form into Yoneda form.

view :: Lens s s a a -> s -> a Source #

Read the focus, discarding residual.

set :: Lens s t a b -> b -> s -> t Source #

Replace the focus, keeping residual from s.

over :: Lens s t a b -> (a -> b) -> s -> t Source #

Map the focus.

Adapter to polynomial morphisms

morphismAsLens :: Morphism (Mono s s) (Mono i o) -> Lens s s o i Source #

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

lensAsMorphism :: Lens s s o i -> Morphism (Mono s s) (Mono i o) Source #

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)