Store Comonad

definition example theorem program

The store (costate) comonad is the Comonad $L_s\circ R_s$ generated by the Currying adjunction $L_{s}a=a\times s⊣R_{s}c=c^s$ — the other composite of the adjunction that generates the State Monad:

data Store s c = St (s -> c) s              -- an accessor into an "infinite stream" plus the current index
instance Functor (Store s) where fmap g (St f s) = St (g . f) s
instance Comonad (Store s) where
  extract   (St f s) = f s                  -- the counit ε: function application
  duplicate (St f s) = St (St f) s          -- δ = L_s ∘ η ∘ R_s

With s = Int, f is an infinite array and s the current position: duplicate gives the stream of all shifted views, extend convolves a co-Kleisli arrow Store s c -> d over the whole store (lazily). Store Double recovers the continuous Signal comonad.

Sources: DaoFP §16.3 (“Costate comonad”, “Comonad coalgebras”, “Lenses”), Exercise 16.3.1 (cellular automaton, rule 110); §15.3 (the currying adjunction).

Deriving $\delta$ by whiskering. With Pair c = (c, Int) for $L$ and Fun c = Int -> c for $R$, the unit is eta :: c -> Fun (Pair c); eta c = \s -> P (c, s), and $\delta =L\circ \eta \circ R$ is delta = fmap @Pair eta :: Pair (Fun c) -> Pair (Fun (Pair (Fun c))), i.e. delta (P (f, s)) = P (\s' -> P (f, s'), s) — right whiskering picks the component at Fun c, left whiskering lifts by fmap of Pair.

Coalgebras are lenses. A comonad coalgebra phi :: s -> Store a s is a pair set :: s -> a -> s, get :: s -> a — a Lens with source s and focus a; the coalgebra laws are exactly the lens laws set/get, set/set, get/set.

Cellular automata (DaoFP Exercise 16.3.1): rule 110 is the co-Kleisli arrow step :: Store Int Cell -> Cell looking at f (n-1), f n, f (n+1); generations are iterate (extend step) initial.

JuliaLeanHaskell

Docs: plain Julia — Catlab has no dedicated API for this; related: Catlab v0.16 docs · GATlab standard library

# Store Int c as (accessor, index); extract, duplicate, extend
struct Store; f::Function; s::Int; end
extract(w::Store) = w.f(w.s)
duplicate(w::Store) = Store(s -> Store(w.f, s), w.s)
extend(g, w::Store) = Store(s -> g(Store(w.f, s)), w.s)
# rule 110 (Exercise 16.3.1): cells indexed by Int, live = true
step(w::Store) = (w.f(w.s - 1), w.f(w.s), w.f(w.s + 1)) in ((true,true,true), (true,false,false), (false,false,false)) ? false : true
init = Store(n -> n == 0, 0)
gens = accumulate((w, _) -> extend(step, w), 1:5; init=init)
[[extract(Store(g.f, n)) ? '#' : '.' for n in -6:2] |> String for g in gens]

import Mathlib
-- Store s c := (s → c) × s with extract = eval and duplicate = (fun s' => (f, s'), s)
def Store (s c : Type) := (s → c) × s
def Store.extract (w : Store s c) : c := w.1 w.2
def Store.duplicate (w : Store s c) : Store s (Store s c) := (fun s' => (w.1, s'), w.2)

data Store s c = St (s -> c) s
instance Functor (Store s) where fmap g (St f s) = St (g . f) s
instance Comonad (Store s) where
  extract (St f s) = f s
  duplicate (St f s) = St (St f) s
 
data Cell = L | D deriving Show
step :: Store Int Cell -> Cell              -- rule 110
step (St f n) = case (f (n - 1), f n, f (n + 1)) of
  (L, L, L) -> D
  (L, D, D) -> D
  (D, D, D) -> D
  _         -> L
generations :: Store Int Cell -> [Store Int Cell]
generations = iterate (extend step)