diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..a1d3540 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake . -Lv diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..96b0e84 --- /dev/null +++ b/.gitignore @@ -0,0 +1,13 @@ +# direnv +.direnv/ + +# Agda build artifacts +*.agdai +MAlonzo/ + +# Nix +result +result-* + +# Draft (personal) +email-draft-to-conal.md diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..e6323fb --- /dev/null +++ b/flake.lock @@ -0,0 +1,77 @@ +{ + "nodes": { + "felix": { + "flake": false, + "locked": { + "lastModified": 1769366763, + "narHash": "sha256-9YB8x9OPAvKnN2b1wI959cjKGO9ay3ef9OgLWHxZCNA=", + "owner": "conal", + "repo": "felix", + "rev": "939c59bffc3fcfa4c2e70fb1dddef193c6a01819", + "type": "github" + }, + "original": { + "owner": "conal", + "repo": "felix", + "type": "github" + } + }, + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1772408722, + "narHash": "sha256-rHuJtdcOjK7rAHpHphUb1iCvgkU3GpfvicLMwwnfMT0=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "f20dc5d9b8027381c474144ecabc9034d6a839a3", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1774401208, + "narHash": "sha256-b8+sRHuVrDhU0/pBKPRS6U8AzLjQdAw5iYcH3NbYCX4=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "a8526804aa49e877887c87dbd7327c08b43eb45f", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1772328832, + "narHash": "sha256-e+/T/pmEkLP6BHhYjx6GmwP5ivonQQn0bJdH9YrRB+Q=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "c185c7a5e5dd8f9add5b2f8ebeff00888b070742", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" + } + }, + "root": { + "inputs": { + "felix": "felix", + "flake-parts": "flake-parts", + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..f87c285 --- /dev/null +++ b/flake.nix @@ -0,0 +1,124 @@ +{ + inputs = { + nixpkgs.url = "github:nixos/nixpkgs"; + flake-parts.url = "github:hercules-ci/flake-parts"; + felix = { + url = "github:conal/felix"; + flake = false; + }; + }; + + outputs = inputs@{ self, nixpkgs, flake-parts, ... }: + flake-parts.lib.mkFlake { inherit inputs; } { + systems = [ "x86_64-linux" "aarch64-linux" ]; + perSystem = { self', system, pkgs, ... }: { + devShells.default = + let + agdaWithStdlib = pkgs.agda.withPackages (p: [ p.standard-library ]); + felixCompiled = pkgs.stdenv.mkDerivation { + name = "felix-compiled"; + src = inputs.felix; + nativeBuildInputs = [ agdaWithStdlib ]; + buildPhase = '' + mkdir -p $out/src + cp -r src/. $out/src/ + cd $out + agda -i src -i ${pkgs.agdaPackages.standard-library}/src src/Felix/Homomorphism.agda + ''; + installPhase = ":"; + }; + myAgda = pkgs.symlinkJoin { + name = "agda-with-felix"; + paths = [ agdaWithStdlib ]; + buildInputs = [ pkgs.makeWrapper ]; + postBuild = '' + wrapProgram $out/bin/agda \ + --add-flags "-i ${felixCompiled}/src" + ''; + }; + in + pkgs.mkShell { + nativeBuildInputs = [ + myAgda + pkgs.glibcLocales + ]; + shellHook = '' + export LOCALE_ARCHIVE="${pkgs.glibcLocales}/lib/locale/locale-archive" + export LC_ALL="en_US.UTF-8" + echo "Agda ready. Compile with:" + echo " agda --compile limited-recursion/telomare.agda" + ''; + }; + + packages.default = + let + stdlib = pkgs.agdaPackages.standard-library; + in + pkgs.stdenv.mkDerivation { + name = "agda-telomare"; + src = pkgs.lib.cleanSource ./limited-recursion; + nativeBuildInputs = [ pkgs.agda pkgs.ghc pkgs.glibcLocales ]; + LOCALE_ARCHIVE = "${pkgs.glibcLocales}/lib/locale/locale-archive"; + LC_ALL = "en_US.UTF-8"; + buildPhase = '' + cp -r ${inputs.felix}/src felix-src + chmod -R u+w felix-src + agda -i ${stdlib}/src -i felix-src --compile telomare.agda + ''; + installPhase = '' + mkdir -p $out/bin + cp telomare $out/bin/agda-telomare + ''; + }; + + apps.default = { + type = "app"; + program = "${self'.packages.default}/bin/agda-telomare"; + }; + + checks.fib = pkgs.runCommand "check-fib" { + LOCALE_ARCHIVE = "${pkgs.glibcLocales}/lib/locale/locale-archive"; + LC_ALL = "en_US.UTF-8"; + } '' + actual=$(${self'.packages.default}/bin/agda-telomare) + expected=$(cat <<'EXPECTED' +── Object-language fibonacci (§11): syntax → ⟦_⟧ → run ── +fibS( 0) = 0 [tel remaining: 1] +fibS( 1) = 1 [tel remaining: 1] +fibS( 5) = 5 [tel remaining: 1] +fibS(10) = 55 [tel remaining: 1] +Out-of-tel: fibS(10) with tel 5 → ? + +── Semantic-domain fibonacci (§12): direct Kleisli ── +fib( 0) = 0 [tel remaining: 1] +fib( 1) = 1 [tel remaining: 1] +fib( 2) = 1 [tel remaining: 1] +fib( 3) = 2 [tel remaining: 1] +fib( 4) = 3 [tel remaining: 1] +fib( 5) = 5 [tel remaining: 1] +fib( 6) = 8 [tel remaining: 1] +fib( 7) = 13 [tel remaining: 1] +fib( 8) = 21 [tel remaining: 1] +fib( 9) = 34 [tel remaining: 1] +fib(10) = 55 [tel remaining: 1] + +Out-of-tel: fib(10) with tel 5 → ? +EXPECTED + ) + if [ "$actual" = "$expected" ]; then + echo "PASS: fibonacci output matches expected" + mkdir -p $out + echo "$actual" > $out/result.txt + else + echo "FAIL: output mismatch" + echo "=== Expected ===" + echo "$expected" + echo "=== Actual ===" + echo "$actual" + diff <(echo "$expected") <(echo "$actual") || true + exit 1 + fi + ''; + }; + }; +} diff --git a/limited-recursion/README.md b/limited-recursion/README.md new file mode 100644 index 0000000..5b7752c --- /dev/null +++ b/limited-recursion/README.md @@ -0,0 +1,460 @@ +# Telomare — Agda Specification + +A denotational specification of Telomare's semantics in Agda, following +Conal Elliott's **Denotational Design** and **Type Class Morphisms** methodology. + +--- + +## The central idea + +Every Telomare computation has a **telomere** — a natural number that strictly +decreases on every recursive call. When it reaches zero the program halts +gracefully. This single design decision gives three things for free: + +- **Totality** — all programs terminate, by construction +- **Time bound** — steps taken ≤ initial tel +- **Space bound** — call depth ≤ initial tel, so space = O(tel) + +--- + +## Denotational Design (Elliott's methodology) + +Denotational Design (Conal Elliott, ICFP 2009) says: + +> Choose a mathematical model for your types first. +> Derive every operation as a homomorphism with respect to that model. +> Laws come for free; abstraction leaks become detectable failures. + +The methodology has four steps: + +1. **Pick a semantic model** — assign a precise mathematical meaning to every + type before writing any implementation. +2. **Specify operations as homomorphisms** — require that the meaning function + commutes with every operation: `⟦f a⟧ = f' ⟦a⟧`. +3. **Calculate implementations** — the homomorphism equations often determine + the implementation uniquely. No guessing. +4. **Laws are inherited** — if the model satisfies a law (e.g. monad + associativity), every derived instance satisfies it too. + +### Applied to Telomare + +**Step 1 — the model.** The meaning of a computation returning type `A` is: + +``` +⟦ e : A ⟧ : Tel → Maybe (A × Tel) where Tel = ℕ +``` + +- Input `Tel`: the telomere available at the start. +- Output `just (v, g')`: succeeded, produced `v`, `g'` tel remains. +- Output `nothing`: telomere exhausted — graceful halt. + +This is `StateT Tel Maybe`, a standard mathematical object. We name it `TelM`: + +```agda +TelM : Set → Set +TelM A = Tel → Maybe (A × Tel) +``` + +**Step 2–3 — derive the operations.** +Asking "what must `return` and `bind` be so that `⟦·⟧` is a monad +homomorphism?" yields the only possible answers: + +```agda +return-tel a g = just (a , g) -- 0 tel consumed +bind-tel m f g = m g >>= λ (a, g') → f a g' -- thread tel through +step m zero = nothing -- telomere exhausted +step m (suc g) = m g -- consume 1, continue +``` + +None of these were invented — they were *calculated* from the model. + +### Where the homomorphism requirement appears in the code + +The equation `⟦f a⟧ = f' ⟦a⟧` shows up in three places, at different levels +of explicitness: + +**§2 — implicitly, through derivation.** +`return-tel` and `bind-tel` are the unique solutions to the homomorphism +equations for the `Monad` structure. The requirement is: + +``` +⟦ return a ⟧ = return-tel ⟦a⟧ +⟦ m >>= f ⟧ = ⟦m⟧ >>= (⟦·⟧ ∘ f) +``` + +Solving for what `return` and `>>=` must be on `TelM` forces exactly the +definitions written. Any other definition would violate the equation. + +**§3 — explicitly in the type denotation.** + +```agda +⟦ A ⇒ B ⟧T = ⟦ A ⟧T → TelM ⟦ B ⟧T +``` + +This line *is* a homomorphism equation for the function type constructor `⇒`: + +``` +⟦ A ⇒ B ⟧ = ⟦A⟧ →K ⟦B⟧ +``` + +Writing `⟦ A ⇒ B ⟧T = ⟦A⟧T → ⟦B⟧T` (a plain function) would violate the +homomorphism — function application would not commute with `⟦·⟧` because tel +consumption would be lost. + +**§8 — explicitly proved as Agda propositions.** + +```agda +left-id : (idK ∘K f) a t ≡ f a t +right-id : (f ∘K idK) a t ≡ f a t +``` + +These are the Kleisli category laws written as literal `≡` propositions. +Both proofs proceed by case analysis on `f a t` and then `refl` in each case — +the equations hold *definitionally* within each branch. + +**Summary table:** + +| Location | Operation | Homomorphism equation | +|---|---|---| +| §2 | `return` | `⟦ return a ⟧ t = just (a, t)` | +| §2 | `bind` | `⟦ m >>= f ⟧ = ⟦m⟧ >>= ⟦f⟧` with tel threading | +| §3 | `⇒` type | `⟦ A ⇒ B ⟧ = ⟦A⟧ →K ⟦B⟧` | +| §8 | `id` (left) | `⟦ id ∘ f ⟧ ≡ idK ∘K ⟦f⟧` | +| §8 | `id` (right) | `⟦ f ∘ id ⟧ ≡ ⟦f⟧ ∘K idK` | + +§2 and §3 are where the **derivation** happens (calculate what operations must +be); §8 is where the **verification** happens (prove the equations hold). + +**Step 4 — laws for free.** +Monad laws (left/right identity, associativity) hold on `TelM` because they +hold on `StateT Tel Maybe`. The Kleisli category laws are proved in §8, and +the full lawful category instance (including associativity and congruence) is +assembled in §9f. + +--- + +## The Kleisli Category + +Once `TelM` is chosen as the semantic domain, a category of programs falls +out automatically — the **Kleisli category of `TelM`**. + +| Component | Definition | +|---|---| +| **Objects** | Agda `Set`s (denotations of Telomare types) | +| **Morphisms** `A →K B` | `A → TelM B` = `A → Tel → Maybe (B × Tel)` | +| **Identity** `idK` | `return-tel` — zero tel, passes everything through | +| **Composition** `g ∘K f` | run `f`, thread remaining tel into `g` | +| **Pairing** `forkK f g` | run `f` then `g` on same input, costs add sequentially | +| **Projections** `exlK`, `exrK` | extract from pair, zero tel | + +This category is **Cartesian** (has products). `fixT` adds a feedback +operator on top: the tel is the trace resource that bounds the feedback depth. + +### The category is the denotational design + +These are not two separate things. The category is the semantic model given +its full algebraic structure: + +- **Objects** are denotations of types. +- **Morphisms** are denotations of programs. +- The **TCM** (**Type Class Morphism**) **principle** (homomorphism requirement) + is exactly the **functor condition**: `⟦·⟧` is a functor from the syntactic + category of programs to the Kleisli category of `TelM`. + A TCM is a function `h : A → B` that is a homomorphism for a given type + class — the class structure on `A` corresponds to the class structure on `B` + via `h`. Here `h = ⟦·⟧`. + +``` +⟦ id ⟧ = idK -- identity preserved +⟦ g ∘ f ⟧ = ⟦g⟧ ∘K ⟦f⟧ -- composition preserved +⟦ fork f g ⟧ = forkK ⟦f⟧ ⟦g⟧ +``` + +Each equation says the denotation doesn't leak — meaning of a composition +equals composition of meanings. This is compositional semantics, and the +category is what makes compositionality precise. + +--- + +## Type Class Morphisms (TCM principle) + +Elliott's TCM principle states: + +> *"The instance's meaning follows the meaning's instance."* + +A function `h : A → B` is a **type class morphism** for class `C` if it is a +homomorphism — i.e. the `C` structure on `A` corresponds to the `C` structure +on `B` via `h`. + +For `Monad`: +``` +h (return a) = return (h a) +h (m >>= f) = h m >>= (h ∘ f) +``` + +In our spec `h = ⟦·⟧` and the monad on the left is Telomare's operational +sequencing; on the right is `TelM`'s `bind-tel`. A violation of this +equation would be an **abstraction leak**: the implementation's behaviour +would diverge from the model, making equational reasoning unsound. + +--- + +## Types and their denotations + +```agda +⟦ unit ⟧T = ⊤ +⟦ bool ⟧T = Bool +⟦ nat ⟧T = ℕ +⟦ A ⊗ B ⟧T = ⟦A⟧T × ⟦B⟧T +⟦ A ⊕ B ⟧T = ⟦A⟧T ⊎ ⟦B⟧T +⟦ A ⇒ B ⟧T = ⟦A⟧T → TelM ⟦B⟧T -- functions live in TelM +``` + +The critical line is the last one: a function type `A ⇒ B` does **not** +denote a plain function `⟦A⟧T → ⟦B⟧T`. It denotes a **morphism** in the +Kleisli category. Applying a function is a computational event that consumes +tel. This is where the telomere enters the type system. + +--- + +## Recursion and totality + +### `fixT` — the only recursion primitive + +```agda +private + fixT-aux : {S R : Set} → Tel → ((S →K R) → S →K R) → S →K R + fixT-aux zero _ _ _ = nothing + fixT-aux (suc f) body s = step (body (fixT-aux f body) s) + +fixT body s g = fixT-aux g body s g +``` + +Every unfolding calls `step`, consuming 1 tel. Agda accepts this via the +**fuel pattern**: `fixT-aux` recurses structurally on its first `Tel` +argument (the fuel), which decreases by 1 on every call. The fuel is tied to +the computational tel so the bound is tight. + +There is also `fix` (§5), the special case where input and output types are +the same (`S = R`), which does not call `step` internally — the body is +expected to include its own `step` calls. + +### Totality theorem + +`TelM A = Tel → Maybe (A × Tel)` is a **total** Agda function. There is no +`⊥`, no coinduction, no partiality at the meta-level. The only "failure" is +`nothing`, a legitimate mathematical value meaning "tel ran out". This holds +by construction — no proof needed beyond the type. + +### Complexity bounds + +For a computation run with initial tel `g₀`: + +``` +tel consumed = number of `step` calls ≤ g₀ +call depth ≤ g₀ +space = O(g₀ × frame size) +``` + +These bounds are read directly from the initial tel — no separate complexity +analysis required. + +--- + +## Limited recursion: `{x, y, z}` in Telomare + +Telomare's surface syntax for recursion is: + +``` +{ x , y , z } v +``` + +where: +- `x` — test: if truthy, keep recursing; if falsy, take the base case +- `y` — body: receives `recur` (the recursive continuation) explicitly +- `z` — base: the answer returned when `x` fails + +Unfolding: +``` +{ x , y , z } v = if x(v) then y (fix {...}) v + else z v +``` + +This is **not a new primitive**. It is `fixT` with a guard. In the Agda +code, this pattern is expressed directly using `fixT` with an inline +conditional rather than a separate combinator: + +```agda +fixT (λ recur s → + if test s then body recur s + else base s) +``` + +### Examples from the Telomare standard library + +``` +-- d2c (data-to-Church numeral) +d2c = \n f b -> { id + , \recur i -> f (recur (left i)) + , \i -> b + } n + +-- gcd (Euclidean algorithm) +gcd = \a b -> { \p -> not (dEqual (right p) 0) + , \recur p -> recur (right p, dMod (left p) (right p)) + , \p -> left p + } (a, b) + +-- map over a linked list +map = \f -> { id + , \recur l -> (f (left l), recur (right l)) + , \l -> 0 + } +``` + +In each case: +- The test `x` tells the telomere whether to keep unwinding. +- Each recursive call costs 1 tel (via `fixT-aux`'s `step`). +- The tel consumed equals the number of successful test evaluations. + +--- + +## Fibonacci: two implementations + +The Agda file contains two fibonacci implementations that compute the same +values, demonstrating the full pipeline at different levels. + +### §11 — Object-language fibonacci (syntax → ⟦\_⟧ → run) + +Written entirely in the syntax category `_⇨S_` using point-free categorical +combinators, then denoted into the Kleisli category via `⟦_⟧` and executed. +This is the full pipeline: + +``` +syntax term ─⟦_⟧─▸ Kleisli morphism ─run─▸ Result +``` + +The code defines `fibS : nat ⇨S nat` as a composition of `fixTS` with an +initial-state setup morphism. The point-free style is verbose — this is +exactly what "Compiling to Categories" (Elliott, ICFP 2017) automates away. + +### §12 — Semantic-domain fibonacci (direct Kleisli) + +The same computation written directly as a Kleisli morphism, bypassing the +syntax category. Much shorter, but without the machine-checked homomorphism: + +```agda +FibState = ℕ × ℕ × ℕ -- (counter, a = fib_k, b = fib_{k+1}) + +fib : ℕ →K ℕ +fib n = fixT {S = FibState} {R = ℕ} + (λ recur s → + let cnt = proj₁ s + a = proj₁ (proj₂ s) + b = proj₂ (proj₂ s) + in if isNonZero cnt + then recur (predℕ cnt , b , a + b) + else return-tel a) + (n , 0 , 1) +``` + +This is the `{x, y, z}` limited-recursion pattern expressed directly with +`fixT` and an inline conditional. + +### Output + +Running with `tel = n + 2` (one spare): + +``` +fib( 0) = 0 [tel remaining: 1] +fib( 1) = 1 [tel remaining: 1] +fib( 2) = 1 [tel remaining: 1] +fib( 3) = 2 [tel remaining: 1] +fib( 4) = 3 [tel remaining: 1] +fib( 5) = 5 [tel remaining: 1] +fib( 6) = 8 [tel remaining: 1] +fib( 7) = 13 [tel remaining: 1] +fib( 8) = 21 [tel remaining: 1] +fib( 9) = 34 [tel remaining: 1] +fib(10) = 55 [tel remaining: 1] + +Out-of-tel: fib(10) with tel 5 → ? +``` + +Tel consumed = `n + 1` exactly. The telomere is a tight bound, not a loose one. + +--- + +## Felix integration + +[Felix](https://github.com/conal/felix) is Conal Elliott's Agda library for +categorical denotational design. It provides the modules that `telomare.agda` +imports: + +| Module | What it contributes | +|---|---| +| `Felix.Object` | `Products` / `Coproducts` type-class interfaces | +| `Felix.Equiv` | `Equivalent` — setoid-based morphism equality | +| `Felix.Raw` | `Category` (raw) — `id` and `_∘_` without laws | +| `Felix.Laws` | `Category` (lawful) — identity and associativity laws | +| `Felix.Homomorphism` | `CategoryH` — functors between lawful categories | + +### What Felix guarantees + +Felix's `CategoryH` record bundles three machine-checked obligations: + +```agda +record CategoryH (src tgt : Cat) where + field + F-cong : f ≈ g → Fₘ f ≈ Fₘ g -- preserves equivalence + F-id : Fₘ id ≈ id -- preserves identity + F-∘ : Fₘ (g ∘ f) ≈ Fₘ g ∘ Fₘ f -- preserves composition +``` + +Filling `⟦⟧-CategoryH` (§10g) makes the **TCM equations machine-checked**: +Agda will reject any denotation function `⟦_⟧` that fails to be a functor +from the syntax category `_⇨S_` into the Kleisli category `_→K_`. + +### Why this matters + +Without Felix a proof obligation like `⟦ g ∘S f ⟧ = ⟦g⟧ ∘K ⟦f⟧` would be an +informal convention. With `CategoryH` it is a **type error** to violate it. +Concretely: + +- `F-∘` holding by `refl` (§10g) means compositionality is **definitional**, + not just propositional — no proof term is needed. +- `F-id` holding by `refl` means the identity axiom is also definitional. +- `F-cong` (the inductive proof in `⟦⟧-cong`, §10f) ensures the denotation + respects the equational theory of the syntax category, closing the + abstraction under rewriting. + +--- + +## File structure (`telomare.agda`) + +| Section | Content | +|---|---| +| §1 | Semantic model — `Tel`, `TelM` | +| §2 | Monad operations — `return-tel`, `bind-tel`, `step` | +| §3 | Object language types and their denotations `⟦_⟧T` | +| §4 | Kleisli category — `→K`, `idK`, `∘K`, `forkK`, `exlK`, `exrK` | +| §5 | Recursion primitives — `fix`, `fixT` (fuel pattern) | +| §6 | Complexity bounds | +| §7 | Totality — `run`, `Result` | +| §8 | Kleisli category laws — `left-id`, `right-id` | +| §9 | Felix integration — `→K-Equiv`, `→K-RawCat`, `→K-RawCart`, `→K-LawCat` | +| §10 | Denotation homomorphism — `_⇨S_`, `_≈S_`, `⟦_⟧`, `⟦⟧-CategoryH` | +| §11 | Object-language fibonacci — `fibS` (syntax → `⟦_⟧` → run) | +| §12 | Semantic-domain fibonacci — `fib` (direct Kleisli) | +| §13 | `main` — IO runner | + +--- + +## Key references + +- Conal Elliott, *Denotational Design with Type Class Morphisms*, Haskell + Symposium 2009 +- Conal Elliott, *Compiling to Categories*, ICFP 2017 +- Conal Elliott, *The Simple Essence of Automatic Differentiation*, ICFP 2018 +- Conal Elliott, *Generalized Convolution and Efficient Language Recognition*, + arXiv 1903.10677 diff --git a/limited-recursion/telomare.agda b/limited-recursion/telomare.agda new file mode 100644 index 0000000..a2f23d7 --- /dev/null +++ b/limited-recursion/telomare.agda @@ -0,0 +1,621 @@ +-- Telomare: A Denotational Specification of a Total Functional Language +-- Following Conal Elliott's Denotational Design + Type Class Morphisms methodology. +-- +-- Core idea: every computation is a function (Tel → Maybe (a × Tel)). +-- Tel (the "telomere") strictly decreases on each recursive unfolding, +-- guaranteeing totality. Time and space are bounded by initial tel. + +{-# OPTIONS --guardedness #-} +module telomare where + +open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_) +open import Data.Maybe using (Maybe; just; nothing; _>>=_) +open import Data.Product using (_×_; _,_; proj₁; proj₂) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Data.Unit using (⊤; tt) +open import Data.Bool using (Bool; true; false; not; if_then_else_) +open import Function using (_∘_; id) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) +open import Agda.Primitive using (lzero) + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 1. SEMANTIC MODEL (Denotational Design: choose the model first) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- The denotation of every computation is: +-- +-- ⟦ e : τ ⟧ : Tel → Maybe (⟦τ⟧ × Tel) +-- +-- where Tel = ℕ (the "telomere"). +-- • just (v , g') means: produced value v, g' tel remains. +-- • nothing means: telomere exhausted — program halts gracefully. +-- +-- This is the Kleisli category of the monad TelM. + +Tel : Set +Tel = ℕ + +TelM : Set → Set +TelM A = Tel → Maybe (A × Tel) + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 2. TelM IS A MONAD (instances follow from the semantic model — TCM) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- TCM = Type Class Morphism (Elliott, ICFP 2009). +-- A TCM is a function h : A → B that is a homomorphism for a given type class: +-- the class structure on A corresponds to the class structure on B via h. +-- Here h = ⟦·⟧ (the denotation function). +-- +-- TCM principle (Elliott): "the instance's meaning follows the meaning's instance." +-- TelM A ≅ StateT Tel Maybe A, so all instances are derived homomorphically. + +return-tel : {A : Set} → A → TelM A +return-tel a g = just (a , g) -- pure values cost 0 tel + +bind-tel : {A B : Set} → TelM A → (A → TelM B) → TelM B +bind-tel m f g = m g >>= λ { (a , g') → f a g' } + +-- Consume exactly 1 unit of tel (one "step" / one telomere shortening) +step : {A : Set} → TelM A → TelM A +step m zero = nothing -- telomere exhausted +step m (suc g) = m g -- consume 1, continue + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 3. TYPES OF THE OBJECT LANGUAGE +-- ───────────────────────────────────────────────────────────────────────────── + +data Ty : Set where + unit : Ty + bool : Ty + nat : Ty + _⊗_ : Ty → Ty → Ty -- product + _⊕_ : Ty → Ty → Ty -- sum + _⇒_ : Ty → Ty → Ty -- function (costs tel on apply) + +-- Denotation of types as Agda types +⟦_⟧T : Ty → Set +⟦ unit ⟧T = ⊤ +⟦ bool ⟧T = Bool +⟦ nat ⟧T = ℕ +⟦ A ⊗ B ⟧T = ⟦ A ⟧T × ⟦ B ⟧T +⟦ A ⊕ B ⟧T = ⟦ A ⟧T ⊎ ⟦ B ⟧T +⟦ A ⇒ B ⟧T = ⟦ A ⟧T → TelM ⟦ B ⟧T -- functions live in TelM + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 4. THE KLEISLI CATEGORY OF TelM +-- (Compiling to Categories: programs are morphisms in this category) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- Objects : Agda types (or ⟦τ⟧T for object-language types) +-- Morphisms: A →K B = A → TelM B +-- +-- Identity and composition satisfy the category laws provably. + +infixr 0 _→K_ +_→K_ : Set → Set → Set +A →K B = A → TelM B + +idK : {A : Set} → A →K A +idK = return-tel + +_∘K_ : {A B C : Set} → (B →K C) → (A →K B) → (A →K C) +(g ∘K f) a = bind-tel (f a) g + +-- Cartesian structure (fork / projections) +forkK : {A B C : Set} → (A →K B) → (A →K C) → (A →K (B × C)) +forkK f g a = bind-tel (f a) λ b → + bind-tel (g a) λ c → + return-tel (b , c) + +exlK : {A B : Set} → (A × B) →K A +exlK = return-tel ∘ proj₁ + +exrK : {A B : Set} → (A × B) →K B +exrK = return-tel ∘ proj₂ + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 5. THE ONLY RECURSION PRIMITIVE — fix with mandatory tel consumption +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- Every unfolding of fix costs 1 tel. +-- Therefore recursion depth ≤ initial tel. Totality follows immediately. +-- +-- Implementation note: Agda requires structural recursion. We satisfy this +-- with the "fuel" pattern: fix-aux recurses on an explicit Tel fuel argument +-- that decreases by 1 on each unfolding. The computation tel t' is threaded +-- independently. fix ties the fuel to the computation's own tel supply, +-- so the bound is tight: depth ≤ initial tel. + +private + fix-aux : {A : Set} → Tel → ((A →K A) → (A →K A)) → A →K A + fix-aux zero _ _ _ = nothing -- fuel exhausted ⟹ halt + fix-aux (suc f) body a g = body (fix-aux f body) a g + +fix : {A : Set} → ((A →K A) → (A →K A)) → A →K A +fix body a g = fix-aux g body a g +-- The fuel equals the tel: each unfolding reduces both by 1 (via body's +-- internal step calls), keeping the bound tight. + +-- Generalised fixpoint: input type S may differ from output type R. +-- (fix is the special case S = R.) +private + fixT-aux : {S R : Set} → Tel → ((S →K R) → S →K R) → S →K R + fixT-aux zero _ _ _ = nothing + fixT-aux (suc f) body s = step (body (fixT-aux f body) s) + +fixT : {S R : Set} → ((S →K R) → S →K R) → S →K R +fixT body s g = fixT-aux g body s g + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 6. COMPLEXITY BOUNDS (derived from the semantic model) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- Let c : TelM A. Run it with initial tel t₀. +-- +-- Time (steps taken) = t₀ − t_final ≤ t₀ +-- Depth (call depth) ≤ t₀ (each recursive call costs ≥ 1) +-- Space = O(depth × frame) = O(t₀) +-- +-- Formally: if c t₀ = just (v , t_f) then the number of `step` calls ≤ t₀. + +-- Helper: tel consumed +tel-consumed : {A : Set} → TelM A → Tel → Maybe ℕ +tel-consumed c g₀ = c g₀ >>= λ { (_ , gf) → just (g₀ ∸ gf) } + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 7. TOTALITY THEOREM +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- Every TelM computation terminates: it returns just or nothing, never diverges. +-- This holds by construction — TelM A = Tel → Maybe (A × Tel) is a total function. +-- No partiality, no ⊥, no coinduction needed. +-- +-- Proof sketch (by induction on tel): +-- Base: step m 0 = nothing ✓ terminates +-- Step: step m (suc t) = m t (recurse on strictly smaller tel) ✓ + +-- Stated as a proposition: running any TelM computation is decidable. +data Result (A : Set) : Set where + halted : Result A -- out of tel + finished : A → ℕ → Result A -- value + tel remaining + +run : {A : Set} → TelM A → Tel → Result A +run c g with c g +... | nothing = halted +... | just (v , gf) = finished v gf + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 8. TYPE CLASS MORPHISM LAWS (Elliott's TCM principle as propositions) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- The denotation ⟦·⟧ must be a homomorphism for Category: +-- +-- ⟦ id ⟧ ≡ idK +-- ⟦ g ∘ f ⟧ ≡ ⟦g⟧ ∘K ⟦f⟧ +-- +-- Stated for the Kleisli category laws: + +-- Left identity: idK ∘K f ≡ f +left-id : {A B : Set} (f : A →K B) (a : A) (t : Tel) → + (idK ∘K f) a t ≡ f a t +left-id f a t with f a t +... | nothing = refl +... | just (b , t') = refl + +-- Right identity: f ∘K idK ≡ f +right-id : {A B : Set} (f : A →K B) (a : A) (t : Tel) → + (f ∘K idK) a t ≡ f a t +right-id f a t with f a t +... | nothing = refl +... | just (b , t') = refl + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 9. FELIX INTEGRATION (github.com/conal/felix) +-- +-- Felix is Conal Elliott's Agda library for category-theoretic denotational +-- design. It provides formal interfaces — Category, Cartesian, CategoryH — +-- that our Kleisli category of TelM already satisfies. +-- +-- Here we instantiate those interfaces, making the connection explicit: +-- +-- FR.Category _→K_ — raw category (idK and ∘K) +-- FR.Cartesian _→K_ — Cartesian structure (forkK, exlK, exrK) +-- FL.Category _→K_ — lawful category (identity laws + associativity) +-- +-- The denotation function ⟦_⟧ : Telomare syntax → _→K_ would be a +-- FL.Homomorphism.CategoryH, making the TCM principle machine-checkable. +-- ───────────────────────────────────────────────────────────────────────────── + +import Felix.Object as FO +import Felix.Equiv as FE +import Felix.Raw as FR +import Felix.Laws as FL +import Felix.Homomorphism as FH + +-- 9a. Products for Set — needed so Felix knows ⊤ and × for objects +instance + Set-Products : FO.Products Set + Set-Products = record { ⊤ = ⊤ ; _×_ = _×_ } + +-- 9b. Equivalence on Kleisli morphisms: pointwise propositional equality +-- f ≈ g iff ∀ a t → f a t ≡ g a t +instance + →K-Equiv : FE.Equivalent lzero _→K_ + →K-Equiv = record + { _≈_ = λ f g → ∀ a t → f a t ≡ g a t + ; equiv = record + { refl = λ _ _ → refl + ; sym = λ p a t → sym (p a t) + ; trans = λ p q a t → trans (p a t) (q a t) + } + } + +-- 9c. Raw Category: idK and ∘K satisfy Felix's Category interface +instance + →K-RawCat : FR.Category _→K_ + →K-RawCat = record { id = idK ; _∘_ = _∘K_ } + +-- 9d. Raw Cartesian: forkK / exlK / exrK satisfy Felix's Cartesian interface +instance + →K-RawCart : FR.Cartesian _→K_ + →K-RawCart = record { ! = λ _ → return-tel tt ; _▵_ = forkK ; exl = exlK ; exr = exrK } + +-- 9e. Proofs for the lawful Category instance +-- +-- We need three lemmas beyond §8's left-id / right-id: +-- Maybe->>=-assoc : monad associativity for Maybe (needed for assoc-tel) +-- assoc-tel : ((h ∘K g) ∘K f) a t ≡ (h ∘K (g ∘K f)) a t +-- >>=-congˡ : helper for congruence proof +-- ∘≈-tel : h ≈ k → f ≈ g → h ∘K f ≈ k ∘K g (pointwise) + +private + -- Associativity of Kleisli composition by direct case analysis on f a t. + assoc-tel : {A B C D : Set} {f : A →K B} {g : B →K C} {h : C →K D} + → ∀ a t → ((h ∘K g) ∘K f) a t ≡ (h ∘K (g ∘K f)) a t + assoc-tel {f = f} {g} {h} a t with f a t + ... | nothing = refl + ... | just (b , t') with g b t' + ... | nothing = refl + ... | just (c , t'') = refl + + -- Congruence of >>= in the first argument (the Maybe value). + >>=-congˡ : ∀ {α β : Set} (m : Maybe α) {f g : α → Maybe β} + → (∀ x → f x ≡ g x) → (m >>= f) ≡ (m >>= g) + >>=-congˡ nothing _ = refl + >>=-congˡ (just x) pf = pf x + + -- Congruence of Kleisli composition: + -- h ≈ k → f ≈ g → h ∘K f ≈ k ∘K g (all ≈ are pointwise) + ∘≈-tel : ∀ {α β γ : Set} {h k : β →K γ} {f g : α →K β} + → (∀ b t → h b t ≡ k b t) + → (∀ a t → f a t ≡ g a t) + → ∀ a t → (h ∘K f) a t ≡ (k ∘K g) a t + ∘≈-tel {h = h} {g = g} h≈k f≈g a t = + trans (cong (λ m → m >>= λ { (b , t') → h b t' }) (f≈g a t)) + (>>=-congˡ (g a t) λ { (b , t') → h≈k b t' }) + +-- 9f. Lawful Category instance: _→K_ satisfies Felix's Laws.Category +instance + →K-LawCat : FL.Category _→K_ + →K-LawCat = record + { identityˡ = λ {_} {_} {f} → left-id f + ; identityʳ = λ {_} {_} {f} → right-id f + ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → assoc-tel {f = f} {g = g} {h = h} + ; ∘≈ = λ {_} {_} {_} {f} {g} {h} {k} → ∘≈-tel {h = h} {k = k} {f = f} {g = g} + } + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 10. DENOTATION HOMOMORPHISM (the TCM principle, machine-checked) +-- +-- We define Telomare's SYNTAX CATEGORY _⇨S_ and prove that the denotation +-- function ⟦_⟧ is a Felix CategoryH (functor) into the Kleisli category _→K_. +-- +-- This makes the TCM equations machine-checked: +-- +-- ⟦ idS ⟧ = idK (F-id, by definition) +-- ⟦ g ∘S f ⟧ = ⟦g⟧ ∘K ⟦f⟧ (F-∘, by definition) +-- f ≈S g ⟹ ⟦f⟧ ≈ ⟦g⟧ (F-cong, proved below) +-- +-- Any violation would be an abstraction leak: implementation behaviour +-- diverges from the semantic model, making equational reasoning unsound. +-- ───────────────────────────────────────────────────────────────────────────── + +-- 10a. Syntax morphisms — the free category over Telomare's primitives. +-- Objects are Telomare types (Ty); morphisms are terms-in-context. +infix 0 _⇨S_ +data _⇨S_ : Ty → Ty → Set where + idS : {A : Ty} → A ⇨S A + _∘S_ : {A B C : Ty} → (B ⇨S C) → (A ⇨S B) → (A ⇨S C) + !S : {A : Ty} → A ⇨S unit + forkS : {A B C : Ty} → (A ⇨S B) → (A ⇨S C) → (A ⇨S (B ⊗ C)) + exlS : {A B : Ty} → (A ⊗ B) ⇨S A + exrS : {A B : Ty} → (A ⊗ B) ⇨S B + -- Nat primitives + zeroS : unit ⇨S nat + sucS : nat ⇨S nat + predS : nat ⇨S nat + addS : (nat ⊗ nat) ⇨S nat + isNonZeroS : nat ⇨S bool + -- Conditional: test, then-branch, else-branch (all from same input) + condS : {A B : Ty} → (A ⇨S bool) → (A ⇨S B) → (A ⇨S B) → A ⇨S B + -- Function application (cartesian closed structure) + evalS : {A B : Ty} → ((A ⇒ B) ⊗ A) ⇨S B + -- Recursion: body receives (recur, state), returns result + fixTS : {S R : Ty} → (((S ⇒ R) ⊗ S) ⇨S R) → S ⇨S R + +-- 10b. Syntactic equivalence — the equational theory of the syntax category. +-- Identifies morphisms up to the category laws (identity, associativity, +-- congruence) without collapsing to propositional equality on terms. +infix 4 _≈S_ +data _≈S_ : {A B : Ty} → (A ⇨S B) → (A ⇨S B) → Set where + reflS : {A B : Ty} {f : A ⇨S B} + → f ≈S f + symS : {A B : Ty} {f g : A ⇨S B} + → f ≈S g → g ≈S f + transS : {A B : Ty} {f g h : A ⇨S B} + → f ≈S g → g ≈S h → f ≈S h + -- Category laws (generating the equational theory) + ∘-idlS : {A B : Ty} {f : A ⇨S B} + → (idS ∘S f) ≈S f + ∘-idrS : {A B : Ty} {f : A ⇨S B} + → (f ∘S idS) ≈S f + ∘-assS : {A B C D : Ty} {f : A ⇨S B} {g : B ⇨S C} {h : C ⇨S D} + → ((h ∘S g) ∘S f) ≈S (h ∘S (g ∘S f)) + ∘-congS : {A B C : Ty} {f f' : A ⇨S B} {g g' : B ⇨S C} + → g ≈S g' → f ≈S f' → (g ∘S f) ≈S (g' ∘S f') + +-- 10c. Denotation of syntax morphisms into the Kleisli category. +-- ⟦_⟧ maps each syntactic term to its semantic Kleisli morphism. +⟦_⟧ : {A B : Ty} → (A ⇨S B) → (⟦ A ⟧T →K ⟦ B ⟧T) +⟦ idS ⟧ = idK +⟦ g ∘S f ⟧ = ⟦ g ⟧ ∘K ⟦ f ⟧ +⟦ !S ⟧ = λ _ → return-tel tt +⟦ forkS f g ⟧ = forkK ⟦ f ⟧ ⟦ g ⟧ +⟦ exlS ⟧ = exlK +⟦ exrS ⟧ = exrK +⟦ zeroS ⟧ = λ _ → return-tel 0 +⟦ sucS ⟧ = λ n → return-tel (suc n) +⟦ predS ⟧ = λ { zero → return-tel zero ; (suc n) → return-tel n } +⟦ addS ⟧ = λ { (m , n) → return-tel (m + n) } +⟦ isNonZeroS ⟧ = λ { zero → return-tel false ; (suc _) → return-tel true } +⟦ condS test t f ⟧ = λ a → bind-tel (⟦ test ⟧ a) (λ b → if b then ⟦ t ⟧ a else ⟦ f ⟧ a) +⟦ evalS ⟧ = λ { (f , a) → f a } +⟦ fixTS body ⟧ = fixT (λ recur s → ⟦ body ⟧ (recur , s)) + +-- 10d. Felix instances for the syntax category. + +-- Equivalence: use the syntactic equational theory as the setoid. +instance + ⇨S-Equiv : FE.Equivalent lzero _⇨S_ + ⇨S-Equiv = record + { _≈_ = _≈S_ + ; equiv = record { refl = reflS ; sym = symS ; trans = transS } + } + +-- Raw category: idS and _∘S_ directly. +instance + ⇨S-RawCat : FR.Category _⇨S_ + ⇨S-RawCat = record { id = idS ; _∘_ = _∘S_ } + +-- Lawful category: the syntactic laws are the constructors of _≈S_. +instance + ⇨S-LawCat : FL.Category _⇨S_ + ⇨S-LawCat = record + { identityˡ = λ {_} {_} {f} → ∘-idlS {f = f} + ; identityʳ = λ {_} {_} {f} → ∘-idrS {f = f} + ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → ∘-assS {f = f} {g = g} {h = h} + ; ∘≈ = λ {_} {_} {_} {f} {g} {h} {k} → ∘-congS {f = f} {f' = g} {g = h} {g' = k} + } + +-- 10e. Homomorphism structure. + +-- Object map: Ty → Set via ⟦_⟧T. +instance + Ty→Set-Hₒ : FH.Homomorphismₒ Ty Set + Ty→Set-Hₒ = record { Fₒ = ⟦_⟧T } + +-- Morphism map: _⇨S_ → _→K_ via ⟦_⟧. +instance + ⟦⟧-H : FH.Homomorphism _⇨S_ _→K_ + ⟦⟧-H = record { Fₘ = ⟦_⟧ } + +-- 10f. ⟦_⟧ preserves syntactic equivalence (F-cong). +-- Each constructor of _≈S_ maps to the corresponding law on _→K_. +⟦⟧-cong : {A B : Ty} {f g : A ⇨S B} + → f ≈S g + → ∀ a t → ⟦ f ⟧ a t ≡ ⟦ g ⟧ a t +⟦⟧-cong reflS a t = refl +⟦⟧-cong (symS p) a t = sym (⟦⟧-cong p a t) +⟦⟧-cong (transS p q) a t = trans (⟦⟧-cong p a t) (⟦⟧-cong q a t) +⟦⟧-cong (∘-idlS {f = f}) a t = left-id ⟦ f ⟧ a t +⟦⟧-cong (∘-idrS {f = f}) a t = right-id ⟦ f ⟧ a t +⟦⟧-cong (∘-assS {f = f} {g = g} {h = h}) a t = assoc-tel {f = ⟦ f ⟧} {g = ⟦ g ⟧} {h = ⟦ h ⟧} a t +⟦⟧-cong (∘-congS {f = f} {f' = f'} {g = g} {g' = g'} p q) a t = + ∘≈-tel {h = ⟦ g ⟧} {k = ⟦ g' ⟧} {f = ⟦ f ⟧} {g = ⟦ f' ⟧} (⟦⟧-cong p) (⟦⟧-cong q) a t + +-- 10g. THE HOMOMORPHISM THEOREM. +-- ⟦_⟧ is a CategoryH — a functor from the syntax category to _→K_. +-- +-- F-id and F-∘ hold by DEFINITION (refl): the denotation of idS is idK, +-- and the denotation of composition IS Kleisli composition. +-- F-cong is proved by induction on the syntactic equivalence above. +instance + ⟦⟧-CategoryH : FH.CategoryH _⇨S_ _→K_ + ⟦⟧-CategoryH = record + { F-cong = ⟦⟧-cong + ; F-id = λ _ _ → refl -- ⟦ idS ⟧ = idK, definitionally + ; F-∘ = λ _ _ → refl -- ⟦ g ∘S f ⟧ = ⟦g⟧ ∘K ⟦f⟧, definitionally + } + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 11. OBJECT-LANGUAGE FIBONACCI (full pipeline: syntax → ⟦_⟧ → run) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- Here we write fibonacci entirely in the object language (_⇨S_), denote it +-- into the Kleisli category via ⟦_⟧, and run it. This is the full pipeline: +-- +-- syntax term ─⟦_⟧─▸ Kleisli morphism ─run─▸ Result +-- +-- Point-free categorical style is verbose — this is exactly what +-- "Compiling to Categories" (Elliott, ICFP 2017) automates away. + +-- State type: (counter, (fib_k, fib_{k+1})) +FibStateT : Ty +FibStateT = nat ⊗ (nat ⊗ nat) + +-- The body of the fixpoint. +-- Input type: (recur, (cnt, (a, b))) where recur : FibStateT ⇒ nat +-- If cnt ≠ 0: recur (pred cnt, (b, a + b)) +-- If cnt = 0: return a +private + BodyIn : Ty + BodyIn = (FibStateT ⇒ nat) ⊗ FibStateT + + -- Projections from (recur, (cnt, (a, b))) + recurP : BodyIn ⇨S (FibStateT ⇒ nat) + recurP = exlS + + cntP : BodyIn ⇨S nat + cntP = exlS ∘S exrS + + aP : BodyIn ⇨S nat + aP = exlS ∘S (exrS ∘S exrS) + + bP : BodyIn ⇨S nat + bP = exrS ∘S (exrS ∘S exrS) + + -- New state: (pred cnt, (b, a + b)) + newStateP : BodyIn ⇨S FibStateT + newStateP = forkS (predS ∘S cntP) + (forkS bP (addS ∘S forkS aP bP)) + + -- Apply recur to new state + recurCallP : BodyIn ⇨S nat + recurCallP = evalS ∘S forkS recurP newStateP + +fibBodyS : BodyIn ⇨S nat +fibBodyS = condS (isNonZeroS ∘S cntP) recurCallP aP + +-- The fixpoint: FibStateT → nat +fibInnerS : FibStateT ⇨S nat +fibInnerS = fixTS fibBodyS + +-- Initial state setup: n ↦ (n, (0, 1)) +initStateS : nat ⇨S FibStateT +initStateS = forkS idS (forkS (zeroS ∘S !S) (sucS ∘S (zeroS ∘S !S))) + +-- The complete program: nat → nat +fibS : nat ⇨S nat +fibS = fibInnerS ∘S initStateS + +-- ── Execution: denote then run ──────────────────────────────────────────── +fibS-0 : Result ℕ ; fibS-0 = run (⟦ fibS ⟧ 0) 2 +fibS-1 : Result ℕ ; fibS-1 = run (⟦ fibS ⟧ 1) 3 +fibS-5 : Result ℕ ; fibS-5 = run (⟦ fibS ⟧ 5) 7 +fibS-10 : Result ℕ ; fibS-10 = run (⟦ fibS ⟧ 10) 12 + +fibS-10-starved : Result ℕ +fibS-10-starved = run (⟦ fibS ⟧ 10) 5 + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 12. FIBONACCI IN THE SEMANTIC DOMAIN (for comparison) +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- The same computation, but written directly as a Kleisli morphism — +-- bypassing the syntax category. Much shorter, but no machine-checked +-- homomorphism connecting it to the object language. +-- +-- Iterative Fibonacci using fixT directly: +-- +-- State S = ℕ × ℕ × ℕ (counter, fib_k, fib_{k+1}) +-- Result R = ℕ +-- +-- The body checks the counter: if non-zero, step forward; if zero, return. +-- Each unfolding costs 1 tel (via fixT's step). +-- Tel cost: exactly n + 1 steps. + +private + isNonZero : ℕ → Bool + isNonZero zero = false + isNonZero (suc _) = true + + predℕ : ℕ → ℕ + predℕ zero = zero + predℕ (suc k) = k + +FibState : Set +FibState = ℕ × ℕ × ℕ -- (counter, a = fib_k, b = fib_{k+1}) + +fib : ℕ →K ℕ +fib n = fixT {S = FibState} {R = ℕ} + (λ recur s → + let cnt = proj₁ s + a = proj₁ (proj₂ s) + b = proj₂ (proj₂ s) + in if isNonZero cnt + then recur (predℕ cnt , b , a + b) + else return-tel a) + (n , 0 , 1) + +-- ── Running Fibonacci ─────────────────────────────────────────────────────── + +fib-0 : Result ℕ ; fib-0 = run (fib 0) 2 +fib-1 : Result ℕ ; fib-1 = run (fib 1) 3 +fib-2 : Result ℕ ; fib-2 = run (fib 2) 4 +fib-3 : Result ℕ ; fib-3 = run (fib 3) 5 +fib-4 : Result ℕ ; fib-4 = run (fib 4) 6 +fib-5 : Result ℕ ; fib-5 = run (fib 5) 7 +fib-6 : Result ℕ ; fib-6 = run (fib 6) 8 +fib-7 : Result ℕ ; fib-7 = run (fib 7) 9 +fib-8 : Result ℕ ; fib-8 = run (fib 8) 10 +fib-9 : Result ℕ ; fib-9 = run (fib 9) 11 +fib-10 : Result ℕ ; fib-10 = run (fib 10) 12 + +-- Out-of-tel example: +fib-10-starved : Result ℕ +fib-10-starved = run (fib 10) 5 -- needs 11, given 5 → halted + +-- ───────────────────────────────────────────────────────────────────────────── +-- § 13. MAIN (run fibonacci results via GHC backend) +-- ───────────────────────────────────────────────────────────────────────────── + +open import IO using (IO; putStrLn; Main; _>>_) +open import Data.Nat.Show using (show) +open import Data.String using (String; _++_) + +showVal : Result ℕ → String +showVal halted = "?" +showVal (finished v _) = show v + +showResultRow : String → Result ℕ → String +showResultRow label r = label ++ " = " ++ showVal r + ++ " [tel remaining: " ++ telLeft r ++ "]" + where + telLeft : Result ℕ → String + telLeft halted = "exhausted" + telLeft (finished _ g) = show g + +main : Main +main = IO.run do + putStrLn "── Object-language fibonacci (§11): syntax → ⟦_⟧ → run ──" + putStrLn (showResultRow "fibS( 0)" fibS-0) + putStrLn (showResultRow "fibS( 1)" fibS-1) + putStrLn (showResultRow "fibS( 5)" fibS-5) + putStrLn (showResultRow "fibS(10)" fibS-10) + putStrLn ("Out-of-tel: fibS(10) with tel 5 → " ++ showVal fibS-10-starved) + putStrLn "" + putStrLn "── Semantic-domain fibonacci (§12): direct Kleisli ──" + putStrLn (showResultRow "fib( 0)" fib-0) + putStrLn (showResultRow "fib( 1)" fib-1) + putStrLn (showResultRow "fib( 2)" fib-2) + putStrLn (showResultRow "fib( 3)" fib-3) + putStrLn (showResultRow "fib( 4)" fib-4) + putStrLn (showResultRow "fib( 5)" fib-5) + putStrLn (showResultRow "fib( 6)" fib-6) + putStrLn (showResultRow "fib( 7)" fib-7) + putStrLn (showResultRow "fib( 8)" fib-8) + putStrLn (showResultRow "fib( 9)" fib-9) + putStrLn (showResultRow "fib(10)" fib-10) + putStrLn "" + putStrLn ("Out-of-tel: fib(10) with tel 5 → " ++ showVal fib-10-starved) diff --git a/readme.md b/readme.md index fafcc58..3937408 100644 --- a/readme.md +++ b/readme.md @@ -44,3 +44,121 @@ For mentoring, a typical getting started path looks something like the following If you want to quit, that's fine, but I prefer hearing so explicitly. You can find my email address near the bottom of my [home page](http://conal.net). + +## Setting up an Agda environment with Nix + +This repository provides a Nix flake that supplies Agda with the [standard library](https://github.com/agda/agda-stdlib) and [Felix](https://github.com/conal/felix) (Conal's categorical denotational design library) pre-compiled. +The only prerequisite is [Nix](https://nixos.org/download/) with flakes enabled. + +### 1. Install Nix (if you don't have it) + +The recommended installer is [Determinate Nix](https://determinate.systems/nix-installer/), which already has flakes enabled — no extra configuration needed: + +```bash +curl --proto '=https' --tlsv1.2 -sSf -L https://install.determinate.systems/nix | sh -s -- install +``` + +### 2. Enter the development shell + +From the repository root: + +```bash +nix develop +``` + +This drops you into a shell with `agda` and `agda-mode` on your `PATH`, the standard library available, and [Felix](https://github.com/conal/felix) (Conal's Agda library for categorical denotational design) pre-compiled. +You can now type-check or compile any Agda file in the repository, and `import Felix.*` works without any extra flags. + +### 3. Using direnv (recommended) + +[direnv](https://direnv.net/) activates the Nix devShell automatically when you `cd` into the project, so you don't have to run `nix develop` manually each time. + +Install direnv, then allow the project's `.envrc`: + +```bash +direnv allow +``` + +From now on, entering the project directory will automatically load the Agda environment. + +## Setting up Emacs / Spacemacs for Agda + +Interactive Agda editing in Emacs/Spacemacs relies on three pieces: + +1. **direnv** activates the project's Nix devShell automatically when a file in the repo is opened. +2. The devShell provides the wrapped `agda` binary (with Felix pre-compiled) and the `agda-mode` binary. +3. A hook in your Emacs config defers to the devShell's `agda-mode` instead of any globally-installed one. + +### Prerequisites + +* `direnv` installed and its Emacs integration active (`direnv-mode` or the `envrc` package). +* No separate global `agda` or `agda-mode` install is required — everything comes from the Nix devShell. + +### Spacemacs snippet + +Add the following inside `dotspacemacs/user-config` in your `~/.spacemacs`: + +```elisp +(defun my/maybe-activate-agda-mode () + "Activate agda2-mode for Agda files using the project's direnv environment. +Deferred via idle-timer. Derives the agda2.el path directly from the +agda-mode binary path to avoid shell-command-to-string timing issues." + (when (and (buffer-file-name) + (string-match-p "\\.l?agda\\(?:\\.md\\)?\\'" (buffer-file-name)) + (not (eq major-mode 'agda2-mode))) + (let ((buf (current-buffer))) + (run-with-idle-timer + 0 nil + (lambda () + (when (buffer-live-p buf) + (with-current-buffer buf + (ignore-errors (direnv-update-directory-environment default-directory)) + (when (not (eq major-mode 'agda2-mode)) + (let* ((agda-mode-bin (executable-find "agda-mode")) + (agda2-el (when agda-mode-bin + (car (last + (seq-filter + (lambda (l) (string-suffix-p ".el" l)) + (split-string + (shell-command-to-string + (concat agda-mode-bin " locate")) + "\n" t))))))) + (if (and agda2-el (file-exists-p agda2-el)) + (progn + (add-to-list 'load-path (file-name-directory agda2-el)) + (unless (featurep 'agda2-mode) + (load-file agda2-el)) + (agda2-mode)) + (message "agda2-mode: locate failed (bin=%s locate=%s)" + agda-mode-bin agda2-el))))))))))) + +(add-hook 'find-file-hook #'my/maybe-activate-agda-mode) +``` + +Once this is in place, opening any `.agda` file in the repository will automatically activate `agda2-mode` with the correct environment. +You can then load and type-check the file with `C-c C-l`. + +## Running the limited-recursion example + +The `limited-recursion/` directory contains `telomare.agda`, a denotational specification of Telomare's semantics following Conal's Denotational Design methodology. +See [limited-recursion/README.md](limited-recursion/README.md) for a detailed explanation. + +### Compile and run from the devShell + +```bash +nix develop # or let direnv do it +agda --compile limited-recursion/telomare.agda +./limited-recursion/telomare +``` + +### Build and run with Nix directly (no devShell needed) + +```bash +nix run # builds and runs the limited-recursion example +``` + +### Run the checks + +```bash +nix flake check # verifies fibonacci output matches expected +```