bidirectional-lens-logic Skill

bidirectional-lens-logic

The Logic of Lenses: 4-kind lattice for bidirectional programming

Source

Cybercat Institute: Foundations of Bidirectional Programming III — Jules Hedges, September 2024

The 4-Kind Lattice

Variables have temporal direction — forwards or backwards in time:

Kind : Type
Kind = (Bool, Bool)  -- (covariant, contravariant)

--  Kind          Pair          Scoping Rules
-- ─────────────────────────────────────────────────
--  Covariant     (True, False)  delete, copy
--  Contravariant (False, True)  spawn, merge  
--  Bivariant     (True, True)   all four operations
--  Invariant     (False, False) none (linear)

GF(3) Correspondence

The 4-kind lattice projects onto GF(3) via:

           BIVARIANT (True, True)
              ↙ 0 ↘
    COVARIANT       CONTRAVARIANT
   (True, False)    (False, True)
        +1              -1
              ↘   ↙
           INVARIANT (False, False)
              (linear, no trit)

| Kind | (cov, con) | Trit | Role | Operations | |------|------------|------|------|------------| | Covariant | (T, F) | +1 | Generator | delete, copy | | Contravariant | (F, T) | -1 | Validator | spawn, merge | | Bivariant | (T, T) | 0 | Coordinator | all four | | Invariant | (F, F) | — | Linear | none |

Tensor Product = GF(3) Multiplication

Tensor : Ty (covx, conx) -> Ty (covy, cony)
      -> Ty (covx && covy, conx && cony)

This IS the GF(3) multiplication table:

     | +1    0    -1
─────┼─────────────────
 +1  | +1   +1    0      (True && _ = depends)
  0  | +1    0   -1      (bivariant preserves)
 -1  |  0   -1   -1      (_ && True = depends)

When tensoring covariant (+1) with contravariant (-1):

covx && covy = True && False = False
conx && cony = False && True = False
Result: (False, False) = invariant/linear

This is why +1 ⊗ -1 = 0 gives us linear/invariant behavior!

The Structure Datatype

Context morphisms with kind-aware operations:

data Structure : All Ty kas -> All Ty kbs -> Type where
  Empty  : Structure [] []
  Insert : Parity a b -> IxInsertion a as as' 
        -> Structure as bs -> Structure as' (b :: bs)
  
  -- Covariant operations (forward time)
  Delete : {a : Ty (True, con)} -> Structure as bs -> Structure (a :: as) bs
  Copy   : {a : Ty (True, con)} -> IxElem a as 
        -> Structure as bs -> Structure as (a :: bs)
  
  -- Contravariant operations (backward time)
  Spawn  : {b : Ty (cov, True)} -> Structure as bs -> Structure as (b :: bs)
  Merge  : {b : Ty (cov, True)} -> IxElem b bs 
        -> Structure as bs -> Structure (b :: as) bs

CRDT Operation Mapping

Structure Op    CRDT Operation         Direction
─────────────────────────────────────────────────
Delete          crdt-stop-share-buffer  forward cleanup
Copy            crdt-share-buffer       forward duplicate
Spawn           (new user joins)        backward appearance
Merge           crdt-connect            backward unification
Insert          crdt-edit               linear (invariant)

The Two NotIntro Rules

Critical insight: There are TWO introduction rules for negation, with different operational semantics:

NotIntroCov : {a : Ty (True, con)} -> Term (a :: as) Unit -> Term as (Not a)
NotIntroCon : {a : Ty (cov, True)} -> Term (a :: as) Unit -> Term as (Not a)

For bivariant types, both rules apply but produce different results!

This explains why GF(3) has:

+1 negates to -1 via NotIntroCov
-1 negates to +1 via NotIntroCon
0 can use either rule — but they're operationally distinct

Negation Swaps Variance

Not : Ty (cov, con) -> Ty (con, cov)

Covariant (+1) → Contravariant (-1)
Contravariant (-1) → Covariant (+1)
Bivariant (0) → Bivariant (0) [stable]
Invariant → Invariant [stable]

Integration with Open Games

The play/coplay structure of open games is precisely this bidirectionality:

        ┌───────────────┐
   X ──→│               │──→ Y      (covariant: forward play)
        │    Game G     │
   R ←──│               │←── S      (contravariant: backward coplay)
        └───────────────┘

X, Y: Covariant types (strategies flow forward)
R, S: Contravariant types (utilities flow backward)
Game G: Invariant/linear (must use everything exactly once)

Entropy-Sequencer Connection

The actionable information framework maps here:

H(I_{t+1} | I^t, u)     = covariant (forward prediction)
H(I_{t+1} | ξ, u)       = contravariant (backward from scene)
───────────────────────────────────────────────────────────
I(ξ; I_{t+1})           = invariant (linear combination)

GF(3) Triad

| Trit | Skill | Role | |------|-------|------| | -1 | temporal-coalgebra | Contravariant observation | | 0 | bidirectional-lens-logic | Bivariant coordination | | +1 | free-monad-gen | Covariant generation |

Conservation: (-1) + (0) + (+1) = 0 ✓

Commands

# Typecheck bidirectional term
just bx-typecheck term.idr

# Evaluate with covariant semantics
just bx-eval-cov term.idr

# Evaluate with contravariant semantics  
just bx-eval-con term.idr

# Compare operational difference
just bx-compare term.idr

Related Skills

entropy-sequencer - Actionable information as bidirectional flow
open-games - Play/coplay as cov/con
parametrised-optics-cybernetics - Para(Lens) structure
polysimy-effect-chains - Effect interpretation as context morphism
crdt - Distributed state with bidirectional sync

References

Hedges, "Foundations of Bidirectional Programming I-III" (Cybercat Institute, 2024)
Riley, "Categories of Optics"
Ghani, Hedges et al., "Compositional Game Theory"
Arntzenius, unpublished work on 4-element kind lattice

Cat# Integration

Trit: 0 (ERGODIC)
Home: Prof
Poly Op: ⊗
Kan Role: Adj
Color: #26D826

The skill participates in triads satisfying:

(-1) + (0) + (+1) ≡ 0 (mod 3)

Agent Skills: bidirectional-lens-logic

Install this agent skill to your local

Skill Files