plurigrid 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 = Falseconx && 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:
+1negates to-1viaNotIntroCov-1negates to+1viaNotIntroCon0can 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 flowopen-games- Play/coplay as cov/conparametrised-optics-cybernetics- Para(Lens) structurepolysimy-effect-chains- Effect interpretation as context morphismcrdt- 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)