diff options
Diffstat (limited to 'lambda-calcul/haskell/plan.md')
| -rw-r--r-- | lambda-calcul/haskell/plan.md | 212 |
1 files changed, 143 insertions, 69 deletions
diff --git a/lambda-calcul/haskell/plan.md b/lambda-calcul/haskell/plan.md index 2d8a21b..724b719 100644 --- a/lambda-calcul/haskell/plan.md +++ b/lambda-calcul/haskell/plan.md @@ -7,10 +7,10 @@ participants to actually *change* the parser, evaluator, or type system. The codebase currently consists of: -- **`Minilang.Lambda.Parser`** — Megaparsec parser producing an `AST` (`Sym`, `Abs`, `App`, +- **`Minilang.Lambda.Parser`** — Megaparsec parser producing an `AST` (`Sym`, `Lit`, `Abs`, `App`, `Def`), with `desugar`/`resugar`/`pretty` for round-tripping to `Term`. - **`Minilang.Lambda.Eval`** — Normalisation-by-Evaluation (NbE) evaluator over `Term` - (`Var`, `Lam`, `App`), producing `Value` (`Clos`, `VNeut`). + (`Var`, `Lam`, `App`, `Num`), producing `Value` (`Clos`, `VNeut`, `VNum`). - **`Minilang.Lambda.DeBruijn`** — A separate CBV head-reduction evaluator used by `evalInEnv` at the top level, operating on De Bruijn-indexed terms. - **`Minilang.Lambda.Infer` / `Unify`** — A complete Hindley-Milner type inferencer @@ -22,38 +22,7 @@ The codebase currently consists of: --- -## Extension 1 — Typed mode challenges - -**Difficulty: 1 / 5** - -### What it is - -The Hindley-Milner type inferencer in `Minilang.Lambda.Infer` and `Minilang.Lambda.Unify` -is fully implemented and reachable via `:lang Typed` in the interactive REPL, but is -completely invisible to the challenge system. `evaluateOutputs` in `App.hs` pattern-matches -on `[Bye, Evaluated ast _ _]` and discards the `Type` field entirely. - -### What changes - -- Switch `initialREPL` from `Untyped` to `Typed` for these challenges (one field change). -- Add a parallel `evaluateType` path in `App.hs` that pattern-matches on the `Type` in the - `Evaluated` constructor and compares it against the submitted string using `Unify.pretty`. -- Optionally introduce a second contest endpoint or a `kind: "type"` field in `Challenge` - to distinguish "what does this reduce to?" from "what type does this have?". - -### Example challenges - -| Expression | Expected type | -|---|---| -| `(lam (x) x)` | `a -> a` | -| `(lam (x y) x)` | `a -> b -> a` | -| `(lam (f x) (f (f x)))` | `(a -> a) -> a -> a` | -| `(lam (x) (x x))` | circularity error | -| `(lam (f g x) (f (g x)))` | `(b -> c) -> (a -> b) -> a -> c` | - ---- - -## Extension 2 — Integer literals +## Extension 1 — Integer literals ✅ implemented **Difficulty: 2 / 5** @@ -63,40 +32,58 @@ Add native integer values to the language. An integer literal like `42` or `-7` self-evaluating value — it needs no reduction. This is the smallest possible extension to `Term` and the foundation for all arithmetic extensions that follow. -### What changes +### What was changed **`Minilang.Lambda.Eval`** -- Add `Num Int` to the `Term` and `Value` types. -- `eval`: one new case — a `Num` literal evaluates to `VNum`. -- `readBack`: one new case — `VNum n` reads back as `Num n`. +- Added `Num Int` to `Term` and `VNum Int` to `Value`. +- Added `NNum Int` to `Neutral` so that a number in function position produces a stuck + neutral application rather than a pattern-match failure. +- `eval`: `Num n → VNum n`. +- `apply`: `VNum n` in function position wraps in `VNeut (NApp (NNum n) a)`. +- `readBack`: `VNum n → Num n` and `VNeut (NNum n) → Num n`. **`Minilang.Lambda.DeBruijn`** -- Add `FNum Int` to `DeBruijn`, propagated through `toDeBruijn`, `fromDeBruijn`, - `substitute`, `eval`/`eval'`, and `pretty`. +- Added `FNum Int` to `DeBruijn`, propagated through `fromDeBruijn`, `toDeBruijn`, + `substitute` (numbers are closed values — `substitute` is a no-op), `eval`/`eval'` + (numbers are already values), and `pretty` (rendered via `showNum`). +- `showNum` renders negative integers with `-` immediately preceding the digits and no + intervening space, matching the parser's requirement. **`Minilang.Lambda.Parser`** -- Add `Lit Int` to `AST`. -- Add a `lit` parser rule using `L.signed spaceConsumer L.decimal`, tried before `sym` so - that `-7` is not mistaken for an identifier starting with `-`. -- `desugar`: `Lit n → Num n`. `resugar`: `Num n → Lit n`. `pretty`: `Lit n → pack (show n)`. +- Added `Lit Int` to `AST`. +- Added a `lit` parser rule: optional `char '-'` with **no intervening whitespace** before + `some digitChar`, wrapped in `lexeme`. Tried before `sym` in the `ast` alternation so + that `-7` is consumed as a number rather than as an identifier starting with `-`. +- `desugar`: `Lit n → Num n`. `resugar`: `Num n → Lit n`. +- `pretty`/`prettyInt`: negative integers printed as `-N` (no space), positives as `N`. +- `Arbitrary AST` updated: `genAst` now includes `Lit <$> arbitrary`; `shrink` has a + `Lit _ → []` base case; `Identifier` generator gained a `suchThat` guard excluding + strings whose prefix would be consumed as an integer literal by the parser. + +**Tests** +- `EvalSpec`: 8 new unit tests covering `normalise` and `eval` on `Num` values, identity + through a lambda, constant ignoring an integer, and a number in function position. +- `ParserSpec`: 2 new property tests replacing all unit tests: + - *valid*: `∀ n :: Int. parse (pretty (Lit n)) == Right (Lit n)` + - *invalid*: `∀ n > 0. parse ("- " <> show n) ≠ Right (Lit (-n))` ### Example challenges | Expression | Result | |---|---| | `42` | `42` | -| `(lam (x) x) 99` | `99` | -| `(lam (n) n) -3` | `-3` | +| `((lam (x) x) 99)` | `99` | +| `((lam (n) n) -3)` | `-3` | --- -## Extension 3 — Built-in arithmetic operators +## Extension 2 — Built-in arithmetic operators **Difficulty: 2 / 5** ### What it is -Depends on Extension 2. Add `+`, `-`, `*`, `/`, `mod`, `=`, `<` as first-class built-in +Depends on Extension 1. Add `+`, `-`, `*`, `/`, `mod`, `=`, `<` as first-class built-in functions. The key interpreter challenge beyond the trivial "add a case" is *partial application*: `(+ 1)` must be a valid value — a closure waiting for its second argument — rather than an error. @@ -123,12 +110,12 @@ rather than an error. | `(+ 3 4)` | `7` | | `(* 2 (+ 1 4))` | `10` | | `(- 10 3)` | `7` | -| `(= 3 3)` | `#t` (requires Extension 5) or `True` Church-bool | +| `(= 3 3)` | `#t` (requires Extension 6) or `True` Church-bool | | `(+ 1)` | a partial application — prints as a neutral `(+ 1)` | --- -## Extension 4 — String literals +## Extension 3 — String literals **Difficulty: 2 / 5** @@ -153,7 +140,7 @@ on the escape convention. - `desugar`: `StrLit s → Str s`. `resugar`: `Str s → StrLit s`. - `pretty`: `StrLit s → "\"" <> escapeString s <> "\""`. -**String builtins** (same pattern as Extension 3): `concat`, `length`, `slice`, `str=`. +**String builtins** (same pattern as Extension 2): `concat`, `length`, `slice`, `str=`. ### Example challenges @@ -166,7 +153,94 @@ on the escape convention. --- -## Extension 5 — Boolean literals and `if` +## Extension 4 — Floating-point number literals + +**Difficulty: 2 / 5** + +### What it is + +Add native double-precision floating-point values to the language. A float literal like +`3.14` or `-0.5` is self-evaluating. This is similar to the integer literal extension but +requires careful handling in the parser to distinguish floats from integers (floats always +contain a `.`), and in `pretty` to ensure the printed form is always re-parseable as a +float (e.g. `1.0` rather than `1`). + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Flt Double` to `Term` and `VFlt Double` to `Value`. +- Add `NFlt Double` to `Neutral` so a float in function position produces a stuck neutral + application rather than a pattern-match failure. +- `eval`: `Flt d → VFlt d`. +- `apply`: `VFlt d` in function position wraps in `VNeut (NApp (NFlt d) a)`. +- `readBack`: `VFlt d → Flt d` and `VNeut (NFlt d) → Flt d`. + +**`Minilang.Lambda.DeBruijn`** +- Add `FFlt Double`, propagated through `fromDeBruijn`, `toDeBruijn`, `substitute` + (floats are closed values), `eval`/`eval'`, and `pretty` (via `showFlt`). +- `showFlt` renders the value with enough decimal places that the printed form round-trips + through the parser (always includes a `.`). + +**`Minilang.Lambda.Parser`** +- Add `FltLit Double` to `AST`. +- Parser rule: try the float rule (digits, `.`, digits, optional exponent) *before* the + integer rule so that `3.14` is not partially consumed as the integer `3`. +- `desugar`: `FltLit d → Flt d`. `resugar`: `Flt d → FltLit d`. +- `pretty`/`prettyFlt`: always emit a decimal point; negative floats printed as `-D.D` + (no space), matching the parser's requirement. +- `Arbitrary AST` updated: `genAst` includes `FltLit <$> arbitrary`; `shrink` has a + `FltLit _ → []` base case; the `Identifier` guard is extended to exclude strings that + would be consumed as float literals. + +**Tests** +- `EvalSpec`: unit tests covering `normalise` and `eval` on `Flt` values, identity through + a lambda, constant ignoring a float, and a float in function position. +- `ParserSpec`: property tests mirroring the integer ones: + - *valid*: `∀ d :: Double. parse (pretty (FltLit d)) == Right (FltLit d)` + - *invalid*: `∀ d > 0. parse ("- " <> show d) ≠ Right (FltLit (-d))` + +### Example challenges + +| Expression | Result | +|---|---| +| `3.14` | `3.14` | +| `((lam (x) x) 2.718)` | `2.718` | +| `((lam (n) n) -0.5)` | `-0.5` | + +--- + +## Extension 5 — Typed mode challenges + +**Difficulty: 3 / 5** + +### What it is + +The Hindley-Milner type inferencer in `Minilang.Lambda.Infer` and `Minilang.Lambda.Unify` +is fully implemented and reachable via `:lang Typed` in the interactive REPL, but is +completely invisible to the challenge system. `evaluateOutputs` in `App.hs` pattern-matches +on `[Bye, Evaluated ast _ _]` and discards the `Type` field entirely. + +### What changes + +- Switch `initialREPL` from `Untyped` to `Typed` for these challenges (one field change). +- Add a parallel `evaluateType` path in `App.hs` that pattern-matches on the `Type` in the + `Evaluated` constructor and compares it against the submitted string using `Unify.pretty`. +- Optionally introduce a second contest endpoint or a `kind: "type"` field in `Challenge` + to distinguish "what does this reduce to?" from "what type does this have?". + +### Example challenges + +| Expression | Expected type | +|---|---| +| `(lam (x) x)` | `a -> a` | +| `(lam (x y) x)` | `a -> b -> a` | +| `(lam (f x) (f (f x)))` | `(a -> a) -> a -> a` | +| `(lam (x) (x x))` | circularity error | +| `(lam (f g x) (f (g x)))` | `(b -> c) -> (a -> b) -> a -> c` | + +--- + +## Extension 6 — Boolean literals and `if` **Difficulty: 2 / 5** @@ -201,12 +275,12 @@ A divergent or error-raising expression in the dead branch must not be evaluated | `#t` | `#t` | | `(if #t a b)` | `a` | | `(if #f a b)` | `b` | -| `(if (= 1 1) "yes" "no")` | `"yes"` (requires Extensions 2–4) | +| `(if (= 1 1) "yes" "no")` | `"yes"` (requires Extensions 2, 3) | | `(if #f (omega omega) 42)` | `42` — the divergent branch is not evaluated | --- -## Extension 6 — Array literals +## Extension 7 — Array literals **Difficulty: 3 / 5** @@ -215,7 +289,7 @@ A divergent or error-raising expression in the dead branch must not be evaluated Add `[e1 e2 … en]` syntax for constructing array values. The square-bracket delimiters are currently unused by the parser. Arrays are *eager*: all elements are evaluated at construction time, consistent with CBV. Structural operations (`head`, `tail`, `cons`, -`nth`, `length`, `map`) follow the same partial-application builtin pattern as Extension 3. +`nth`, `length`, `map`) follow the same partial-application builtin pattern as Extension 2. ### What changes @@ -246,11 +320,11 @@ new test here). | `(tail [10 20 30])` | `[20 30]` | | `(cons 0 [1 2])` | `[0 1 2]` | | `(nth 1 [a b c])` | `b` | -| `(map (lam (x) (+ x 1)) [1 2 3])` | `[2 3 4]` (requires Extension 3) | +| `(map (lam (x) (+ x 1)) [1 2 3])` | `[2 3 4]` (requires Extension 2) | --- -## Extension 7 — `quote` and `eval` +## Extension 8 — `quote` and `eval` **Difficulty: 3 / 5** @@ -265,7 +339,7 @@ distinction between *object language* and *meta-language* becomes observable in The hard part is `(eval e)`: the `eval` builtin must receive the current *environment* as a hidden argument. This means the builtin dispatch mechanism must be extended to thread the environment through, which is a non-trivial change to the builtin application architecture -introduced in Extension 3. +introduced in Extension 2. ### What changes @@ -291,11 +365,11 @@ introduced in Extension 3. | `(quote (lam (x) x))` | `(lam (x) x)` (syntax as data) | | `(eval (quote (lam (x) x)))` | `(lam (x) x)` (re-evaluated) | | `(eval (quote ((lam (x) x) y)))` | `y` | -| `(let ((e (quote (+ 1 2)))) (eval e))` | `3` (requires Extension 3) | +| `(let ((e (quote (+ 1 2)))) (eval e))` | `3` (requires Extension 2) | --- -## Extension 8 — `letrec` / recursive definitions +## Extension 9 — `letrec` / recursive definitions **Difficulty: 3 / 5** @@ -303,7 +377,7 @@ introduced in Extension 3. The current `let` desugars to an immediate lambda application, which means bindings cannot refer to themselves or each other. `letrec` allows mutually recursive definitions. Under -CBV this requires either mutable thunks (see Extension 9) or lazy tying-of-the-knot in the +CBV this requires either mutable thunks (see Extension 10) or lazy tying-of-the-knot in the Haskell host. The standard interpreter-level approach is to build a *circular environment*: the closure created for each binding has the entire `letrec` group already in its environment, which in a lazy host language like Haskell can be expressed directly using @@ -328,12 +402,12 @@ environment, which in a lazy host language like Haskell can be expressed directl | Expression | Result | |---|---| -| `(letrec ((f (lam (x) (if (= x 0) 1 (* x (f (- x 1))))))) (f 5))` | `120` (requires Extensions 3, 5) | +| `(letrec ((f (lam (x) (if (= x 0) 1 (* x (f (- x 1))))))) (f 5))` | `120` (requires Extensions 2, 6) | | `(letrec ((even? (lam (n) (if (= n 0) #t (odd? (- n 1))))) (odd? (lam (n) (if (= n 0) #f (even? (- n 1)))))) (even? 4))` | `#t` | --- -## Extension 9 — Mutable references +## Extension 10 — Mutable references **Difficulty: 3 / 5** @@ -366,12 +440,12 @@ updated to thread the store. |---|---| | `(let ((r (ref 0))) (deref r))` | `0` | | `(let ((r (ref 0))) (set! r 42) (deref r))` | `42` | -| `(let ((r (ref 0))) (set! r (+ (deref r) 1)) (deref r))` | `1` (requires Extension 3) | +| `(let ((r (ref 0))) (set! r (+ (deref r) 1)) (deref r))` | `1` (requires Extension 2) | | Show that argument evaluation order is observable when both arguments mutate shared state | order-dependent result | --- -## Extension 10 — Type annotations +## Extension 11 — Type annotations **Difficulty: 3 / 5** @@ -413,7 +487,7 @@ the inferred type with the declared type and reporting mismatches. --- -## Extension 11 — Algebraic data types +## Extension 12 — Algebraic data types **Difficulty: 4 / 5** @@ -460,7 +534,7 @@ of the type system (sum types, product types, type constructors, arity checking) --- -## Extension 12 — `call/cc` +## Extension 13 — `call/cc` **Difficulty: 4 / 5** @@ -505,7 +579,7 @@ to supply an initial continuation (typically `id`). --- -## Extension 13 — Delimited continuations (`reset` / `shift`) +## Extension 14 — Delimited continuations (`reset` / `shift`) **Difficulty: 5 / 5** @@ -528,7 +602,7 @@ maintained as a mutable data structure threaded through `eval`. ### What changes **`Minilang.Lambda.Eval`** -- Prerequisite: Extension 12 (CPS'd evaluator). +- Prerequisite: Extension 13 (CPS'd evaluator). - Change `eval` to carry *two* continuations: the current meta-continuation and the delimited one, or use an explicit stack of `Frame | Reset` markers. - `reset expr`: evaluate `expr` with a fresh inner continuation and the current outer |