|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | += JTV v2 / 007 Reversibility: Designed Fork |
| 5 | +:toc: macro |
| 6 | + |
| 7 | +[.lead] |
| 8 | +A portfolio-level note on the deliberate divergence between JTV v2's canonical |
| 9 | +reversibility model and 007's Phase 1 implementation. This is a designed |
| 10 | +experiment — two languages in this portfolio exploring adjacent points in the |
| 11 | +reversible computation design space, with shared foundations and a clear |
| 12 | +convergence point. |
| 13 | + |
| 14 | +toc::[] |
| 15 | + |
| 16 | +== Context |
| 17 | + |
| 18 | +JTV (Julia the Viper) is the heritage language from which 007 descends. |
| 19 | +JTV v1 (Alpha stage) established the addition-only Data Language — a single |
| 20 | +arithmetic primitive with the thesis that all other arithmetic operations |
| 21 | +are derivable. JTV v2 (Gamma stage) extends this to the Control Language: |
| 22 | +subtraction is not a primitive, it is the inverse of addition, expressed |
| 23 | +as `reverse { x += v }`. |
| 24 | + |
| 25 | +In April 2026, 007's JTV v2 reversibility implementation underwent a |
| 26 | +comprehensive design session closing five open questions about `reversible { }`, |
| 27 | +`reverse { }`, `irreversible { }`, and the `ReversalToken` mechanism. In |
| 28 | +resolving those questions, a deliberate fork from JTV v2's canonical model |
| 29 | +was identified and documented. This file records that fork at the portfolio |
| 30 | +level. |
| 31 | + |
| 32 | +== The Shared Foundation |
| 33 | + |
| 34 | +Both JTV v2 and 007 (all phases) share the following: |
| 35 | + |
| 36 | +[options="header"] |
| 37 | +|=== |
| 38 | +| Mechanism | Description |
| 39 | +| *Linear `ReversalToken`* | Produced by `reversible { }`, consumed by `reverse tok` or `abandon tok`. Pairing is type-enforced, not runtime stack or label lookup. |
| 40 | +| *`ReversalToken<S>` type parameter* | `S` encodes what was captured. Typechecker infers `S` from mutations inside the block. |
| 41 | +| *`Option<ReversalToken>` at branch joins* | Path-sensitive typing at `branch` join points. Asymmetric branches produce `Option<ReversalToken<S>>` automatically. `match` forces exhaustive handling. No lint needed. |
| 42 | +| *`ExternalHandle` static error* | Sending to an external agent inside `reversible { }` without `irreversible { }` wrapping is a compile-time error. Local reversibility only — distributed reversibility is a protocol-level concern. |
| 43 | +| *`irreversible { }` escape* | Explicit annotation for operations with no defined inverse. |
| 44 | +| *Structural sugar* | `reversible { ... } reverse { ... }` desugars to the token form. |
| 45 | +|=== |
| 46 | + |
| 47 | +== The Fork |
| 48 | + |
| 49 | +The divergence is in what the token carries and what `reverse tok` does. |
| 50 | + |
| 51 | +=== JTV v2 Canonical Model |
| 52 | + |
| 53 | +Per-operation reversal. The `ReversalToken` carries a reversal *log* — |
| 54 | +a sequence of `(op, inv(op))` pairs recorded as operations execute. |
| 55 | +`reverse tok` replays the inverse operations in reverse order. |
| 56 | + |
| 57 | +Subtraction is genuinely `reverse { x += v }` at the operation level. |
| 58 | +Each step of the forward computation has a corresponding inverse step. |
| 59 | +This is the Janus tradition: step-by-step invertibility, theoretical |
| 60 | +alignment with Landauer's principle. |
| 61 | + |
| 62 | +=== 007 Phase 1 |
| 63 | + |
| 64 | +Whole-block snapshot restore. The `ReversalToken` carries the pre-block |
| 65 | +values of `@state` fields declared in `reversible_state { }` (or inferred |
| 66 | +by the typechecker from mutations). `reverse tok` restores those field values. |
| 67 | + |
| 68 | +In a purely functional language, local bindings need no snapshotting — |
| 69 | +lexical scope provides this for free. Only `@state` fields need capturing. |
| 70 | +The snapshot approach delivers correct semantics with minimal machinery |
| 71 | +and is statically verified via token linearity. It is not per-operation. |
| 72 | + |
| 73 | +=== 007 Phase 2 (Planned) |
| 74 | + |
| 75 | +Per-operation reversal via `ref T`. Mutable references within `reversible` |
| 76 | +blocks, with a per-operation inverse log. Converges toward JTV v2's model. |
| 77 | +`ref T` is introduced as a deliberate later addition once Phase 1 has been |
| 78 | +proven in use. |
| 79 | + |
| 80 | +== The Experiment Design |
| 81 | + |
| 82 | +[options="header"] |
| 83 | +|=== |
| 84 | +| Question | Evidenced by |
| 85 | +| Is per-operation inversion required to honour the "subtraction as inverse" claim? | JTV v2 usage |
| 86 | +| Is whole-block snapshot sufficient for agent programming in practice? | 007 Phase 1 usage |
| 87 | +| Does `ref T` at Phase 2 feel natural or forced? | 007 Phase 2 implementation |
| 88 | +| Is snapshot a useful pedagogical stage or merely a stepping stone? | Comparison of learning curves |
| 89 | +| Does the convergence hypothesis hold? | 007 Phase 2 vs JTV v2 canonical — if they agree, yes |
| 90 | +|=== |
| 91 | + |
| 92 | +== Comparison with the Reversible Computation Literature |
| 93 | + |
| 94 | +The shared foundation (linear token, type-parameter-encoded state, |
| 95 | +Option-lifting at branches) represents three mechanisms not present in any |
| 96 | +existing reversible programming system: |
| 97 | + |
| 98 | +. *Linear token as unified pairing + snapshot/log carrier* — no existing |
| 99 | + reversible language (Janus, R, Theseus, STM, algebraic effects) uses a |
| 100 | + linear value as both the pairing mechanism and the typed state carrier. |
| 101 | + |
| 102 | +. *Type-parameter-encoded captured state* — `ReversalToken<S>` encodes |
| 103 | + statically what was captured. STM logs are untyped. Janus has no type |
| 104 | + system. Koka's effect rows do not encode captured values. |
| 105 | + |
| 106 | +. *Option-lifting at branch joins* — Janus and R require syntactically |
| 107 | + symmetric branches. STM retries. Effect handlers require explicit |
| 108 | + continuation management. This portfolio's solution falls out of existing |
| 109 | + linear typing rules with zero new machinery. |
| 110 | + |
| 111 | +These are believed to constitute a novel contribution to the reversible |
| 112 | +computation literature, publishable alongside the 007 or JTV v2 language |
| 113 | +papers. |
| 114 | + |
| 115 | +== Cross-References |
| 116 | + |
| 117 | +* `julia-the-viper/docs/language/DESIGN-JTV-V2-REVERSIBILITY.md` — JTV v2 |
| 118 | + canonical model in full |
| 119 | +* `007/docs/session-2026-04-12-jtv-v2-reversibility-design.adoc` — 007's |
| 120 | + five closed design decisions and Phase 1/Phase 2 plan |
| 121 | +* `typell/docs/decisions/0002-reversibility-as-typing-case-study.md` — the |
| 122 | + three type-system collapses as a TypeLL case study |
0 commit comments