diff options
| -rw-r--r-- | lambda-calcul/haskell/challenges.json | 324 | ||||
| -rw-r--r-- | lambda-calcul/haskell/minilang.cabal | 1 | ||||
| -rw-r--r-- | lambda-calcul/haskell/plan.md | 552 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/API.hs | 10 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/App.hs | 6 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/ServerSpec.hs | 4 |
6 files changed, 869 insertions, 28 deletions
diff --git a/lambda-calcul/haskell/challenges.json b/lambda-calcul/haskell/challenges.json index 4c247af..544bf0a 100644 --- a/lambda-calcul/haskell/challenges.json +++ b/lambda-calcul/haskell/challenges.json @@ -1,20 +1,308 @@ [ - {"level":0, "expr": "x"}, - {"level":1, "expr": "y"}, - {"level":2, "expr": "#%foo"}, - {"level":3, "expr": "(lam (x) x)"}, - {"level":4, "expr": "(x y)"}, - {"level":5, "expr": "((lam (x) x) y)"}, - {"level":6, "expr": "((lam (x y) x) z)"}, - {"level":7, "expr": "(((lam (z) x) z) y)"}, - {"level":8, "expr": "((lam (x y) x) z t)"}, - {"level":9, "expr": "((lam (x y) x) z t foo)"}, - {"level":10, "expr": "(let ((id (lam (x) x))) (id z))"}, - {"level":11, "expr": "(let ((id (lam (x) x))) (id z))"}, - {"level":12, "expr": "(let ((False (lam (f t) f))\n (True (lam (f t) t))\n (Not (lam (b) (b True False))))\n (Not True))"}, - {"level":13, "expr": "(let ((False (lam (f t) f))\n (True (lam (f t) t))\n (Not (lam (b) (b True False))))\n (Not (Not True)))"}, - {"level":14, "expr": "(def False (lam (f t) f))\n (def True (lam (f t) t))\n (def Not (lam (b) (b True False)))\n (Not (Not True)))"}, - {"level":15, "expr": "(def False (lam (f t) f))\n (def True (lam (f t) t))\n (def Not (lam (b) (b True False)))"}, - {"level":16, "expr": "(def Or (lam (a b) (a b True)))"}, - {"level":17, "expr": "(Or (Not True) False)"} + { + "level": 0, + "description": "A lone free variable. What does x reduce to?", + "expr": "x", + "answer": "x" + }, + { + "level": 1, + "description": "Another free variable. What does y reduce to?", + "expr": "y", + "answer": "y" + }, + { + "level": 2, + "description": "A free variable with a fancy name. Identifiers can include special characters like #, %, @, etc.", + "expr": "#%foo", + "answer": "#%foo" + }, + { + "level": 3, + "description": "A lambda abstraction: lam (x) x is the identity function. It is already in normal form.", + "expr": "(lam (x) x)", + "answer": "(lam (x) x)" + }, + { + "level": 4, + "description": "A function application where both sides are free variables. (x y) has no redex to reduce.", + "expr": "(x y)", + "answer": "(x y)" + }, + { + "level": 5, + "description": "Apply the identity function to y. ((lam (x) x) y) performs one beta-reduction step.", + "expr": "((lam (x) x) y)", + "answer": "y" + }, + { + "level": 6, + "description": "Multi-argument lambda applied to one argument. lam (x y) x takes two arguments and returns the first (the K combinator). What is the result of applying it to just z?", + "expr": "((lam (x y) x) z)", + "answer": "(lam (y) z)" + }, + { + "level": 7, + "description": "A constant function applied to its argument, then the result applied to y. (lam (z) x) ignores z and always returns the free variable x.", + "expr": "(((lam (z) x) z) y)", + "answer": "(x y)" + }, + { + "level": 8, + "description": "Apply the two-argument K combinator lam (x y) x to both z and t. It selects its first argument.", + "expr": "((lam (x y) x) z t)", + "answer": "z" + }, + { + "level": 9, + "description": "Apply the K combinator to three arguments. Remember that application is left-associative, so this is ((K z t) foo). What does K z t reduce to, and what happens when you apply that to foo?", + "expr": "((lam (x y) x) z t foo)", + "answer": "(z foo)" + }, + { + "level": 10, + "description": "A let-binding introduces a local definition. Here id is bound to the identity function. What does (id z) evaluate to?", + "expr": "(let ((id (lam (x) x))) (id z))", + "answer": "z" + }, + { + "level": 11, + "description": "The same let-binding as level 10. let desugars into an immediate lambda application: ((lam (id) (id z)) (lam (x) x)).", + "expr": "(let ((id (lam (x) x))) (id z))", + "answer": "z" + }, + { + "level": 12, + "description": "Church-encoded booleans: False = lam (f t) f, True = lam (f t) t. A boolean selects one of two arguments — False picks the first, True picks the second. Not flips a boolean by applying it to True and False in swapped order. What is (Not True)?", + "expr": "(let ((False (lam (f t) f))\n (True (lam (f t) t))\n (Not (lam (b) (b True False))))\n (Not True))", + "answer": "(lam (f t) f)" + }, + { + "level": 13, + "description": "Double negation. Applying Not twice should return the original boolean. What is (Not (Not True))?", + "expr": "(let ((False (lam (f t) f))\n (True (lam (f t) t))\n (Not (lam (b) (b True False))))\n (Not (Not True)))", + "answer": "(lam (f t) t)" + }, + { + "level": 14, + "description": "The same boolean logic as level 13, but using top-level def declarations instead of let. def binds names in the global environment for the rest of the program.", + "expr": "(def False (lam (f t) f))\n (def True (lam (f t) t))\n (def Not (lam (b) (b True False)))\n (Not (Not True)))", + "answer": "(lam (f t) t)" + }, + { + "level": 15, + "description": "Three def declarations with no final expression to evaluate. def statements produce no output on their own — they only extend the environment.", + "expr": "(def False (lam (f t) f))\n (def True (lam (f t) t))\n (def Not (lam (b) (b True False)))", + "answer": "" + }, + { + "level": 16, + "description": "Define Or in the global environment. Or a b = a b True: if a is True it selects its first argument (b); if a is False it selects its second argument (True). Again, no expression to evaluate.", + "expr": "(def Or (lam (a b) (a b True)))", + "answer": "" + }, + { + "level": 17, + "description": "Use the previously defined Or and Not (assumed in scope from prior levels). Evaluate (Or (Not True) False). What boolean does this reduce to?", + "expr": "(Or (Not True) False)", + "answer": "(Or (Not True) False)" + }, + { + "level": 18, + "description": "Introduce And. And a b = a False b: if a is True it selects its second argument (b); if a is False it selects its first argument (False). Evaluate (And True True).", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def Or (lam (a b) (a b True)))\n(def And (lam (a b) (a False b)))\n(And True True)", + "answer": "(lam (f t) t)" + }, + { + "level": 19, + "description": "Combine Or, And and Not. Evaluate (And (Or False True) (Not False)). Both sub-expressions must reduce to True for And to return True.", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def Not (lam (b) (b True False)))\n(def Or (lam (a b) (a b True)))\n(def And (lam (a b) (a False b)))\n(And (Or False True) (Not False))", + "answer": "(lam (f t) t)" + }, + { + "level": 20, + "description": "Xor (exclusive or) is True when exactly one argument is True. It can be defined as And (Or a b) (Not (And a b)). Evaluate (Xor True False).", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def Not (lam (b) (b True False)))\n(def And (lam (a b) (a False b)))\n(def Or (lam (a b) (a b True)))\n(def Xor (lam (a b) (And (Or a b) (Not (And a b)))))\n(Xor True False)", + "answer": "(lam (f t) t)" + }, + { + "level": 21, + "description": "Evaluate (Xor False False). Two identical inputs to Xor should always yield False.", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def Not (lam (b) (b True False)))\n(def And (lam (a b) (a False b)))\n(def Or (lam (a b) (a b True)))\n(def Xor (lam (a b) (And (Or a b) (Not (And a b)))))\n(Xor False False)", + "answer": "(lam (f t) f)" + }, + { + "level": 22, + "description": "Church-encoded if-then-else. Because our True selects its second argument and False selects its first, ite must swap the branches: ite c t e = c e t. Evaluate (ite True a b) — which branch is returned?", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def Not (lam (b) (b True False)))\n(def And (lam (a b) (a False b)))\n(def Or (lam (a b) (a b True)))\n(def ite (lam (c t e) (c e t)))\n(ite True a b)", + "answer": "a" + }, + { + "level": 23, + "description": "Evaluate (ite False a b). When the condition is False, the else-branch should be returned.", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def Not (lam (b) (b True False)))\n(def And (lam (a b) (a False b)))\n(def Or (lam (a b) (a b True)))\n(def ite (lam (c t e) (c e t)))\n(ite False a b)", + "answer": "b" + }, + { + "level": 24, + "description": "Church-encoded pairs. pair x y = lam f -> f x y stores two values by passing them to a selector function. fst p = p (lam x y -> x) retrieves the first. Evaluate (fst (pair a b)).", + "expr": "(def pair (lam (x y f) (f x y)))\n(def fst (lam (p) (p (lam (x y) x))))\n(def snd (lam (p) (p (lam (x y) y))))\n(fst (pair a b))", + "answer": "a" + }, + { + "level": 25, + "description": "snd p = p (lam x y -> y) retrieves the second element of a Church pair. Evaluate (snd (pair a b)).", + "expr": "(def pair (lam (x y f) (f x y)))\n(def fst (lam (p) (p (lam (x y) x))))\n(def snd (lam (p) (p (lam (x y) y))))\n(snd (pair a b))", + "answer": "b" + }, + { + "level": 26, + "description": "Pairs can be nested. (pair a (pair b c)) is a pair whose second element is itself a pair. Evaluate (snd (snd (pair a (pair b c)))).", + "expr": "(def pair (lam (x y f) (f x y)))\n(def fst (lam (p) (p (lam (x y) x))))\n(def snd (lam (p) (p (lam (x y) y))))\n(snd (snd (pair a (pair b c))))", + "answer": "c" + }, + { + "level": 27, + "description": "swap exchanges the two elements of a pair: swap p = pair (snd p) (fst p). Evaluate (fst (swap (pair a b))). After swapping, fst should return what was previously snd.", + "expr": "(def pair (lam (x y f) (f x y)))\n(def fst (lam (p) (p (lam (x y) x))))\n(def snd (lam (p) (p (lam (x y) y))))\n(def swap (lam (p) (pair (snd p) (fst p))))\n(fst (swap (pair a b)))", + "answer": "b" + }, + { + "level": 28, + "description": "Church numerals encode natural numbers as higher-order functions: n applies its first argument (the successor step) to its second argument (the base) exactly n times. zero = lam s z -> z applies s zero times. Evaluate (zero f x).", + "expr": "(def zero (lam (s z) z))\n(zero f x)", + "answer": "x" + }, + { + "level": 29, + "description": "two = lam s z -> s (s z) applies s twice. Evaluate (two f x) — you should see f applied to x twice.", + "expr": "(def two (lam (s z) (s (s z))))\n(two f x)", + "answer": "(f (f x))" + }, + { + "level": 30, + "description": "three = lam s z -> s (s (s z)) applies s three times. Evaluate (three f x).", + "expr": "(def three (lam (s z) (s (s (s z)))))\n(three f x)", + "answer": "(f (f (f x)))" + }, + { + "level": 31, + "description": "isZero tests whether a Church numeral is zero. isZero n = n (lam x -> False) True: if n > 0 the step function (lam x -> False) is applied at least once, discarding its argument and returning False; if n = 0 the base True is returned. Evaluate (isZero zero).", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def zero (lam (s z) z))\n(def isZero (lam (n) (n (lam (x) False) True)))\n(isZero zero)", + "answer": "(lam (f t) t)" + }, + { + "level": 32, + "description": "Evaluate (isZero three). Three is not zero, so the step function fires and the result is False.", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def three (lam (s z) (s (s (s z)))))\n(def isZero (lam (n) (n (lam (x) False) True)))\n(isZero three)", + "answer": "(lam (f t) f)" + }, + { + "level": 33, + "description": "The I combinator (identity): I x = x. It is the simplest combinator and the building block of the SKI calculus. Evaluate (I a).", + "expr": "(def I (lam (x) x))\n(I a)", + "answer": "a" + }, + { + "level": 34, + "description": "The K combinator (constant): K x y = x. It ignores its second argument and always returns its first. Evaluate (K a b).", + "expr": "(def K (lam (x y) x))\n(K a b)", + "answer": "a" + }, + { + "level": 35, + "description": "The S combinator (substitution): S f g x = f x (g x). It distributes its third argument over two functions and applies the results. Evaluate (S f g x) — f and g are free variables here.", + "expr": "(def S (lam (f g x) ((f x) (g x))))\n(S f g x)", + "answer": "(f x (g x))" + }, + { + "level": 36, + "description": "SKI completeness: S K K encodes the identity function. S K K x = K x (K x) = x. Evaluate (S K K a) and confirm it equals a.", + "expr": "(def S (lam (f g x) ((f x) (g x))))\n(def K (lam (x y) x))\n(S K K a)", + "answer": "a" + }, + { + "level": 37, + "description": "The B combinator (composition): B f g x = f (g x). It is function composition. Evaluate (B f g x) — you should see f applied to the result of g applied to x.", + "expr": "(def B (lam (f g x) (f (g x))))\n(B f g x)", + "answer": "(f (g x))" + }, + { + "level": 38, + "description": "The C combinator (flip): C f x y = f y x. It flips the order of the last two arguments of a function. Evaluate (C f a b).", + "expr": "(def C (lam (f x y) (f y x)))\n(C f a b)", + "answer": "(f b a)" + }, + { + "level": 39, + "description": "The W combinator (duplication): W f x = f x x. It applies f to x twice, duplicating the argument. Evaluate (W f a).", + "expr": "(def W (lam (f x) (f x x)))\n(W f a)", + "answer": "(f a a)" + }, + { + "level": 40, + "description": "Scott-encoded lists. nil = lam c n -> n (the empty list). cons h t = lam c n -> c h t stores head and tail directly. head l = l (lam h t -> h) nil extracts the first element. Evaluate (head (cons a nil)).", + "expr": "(def nil (lam (c n) n))\n(def cons (lam (h t c n) (c h t)))\n(def head (lam (l) (l (lam (h t) h) nil)))\n(head (cons a nil))", + "answer": "a" + }, + { + "level": 41, + "description": "tail l = l (lam h t -> t) nil retrieves the rest of a Scott-encoded list. Evaluate (head (tail (cons a (cons b nil)))) — the head of the tail of a two-element list is its second element.", + "expr": "(def nil (lam (c n) n))\n(def cons (lam (h t c n) (c h t)))\n(def head (lam (l) (l (lam (h t) h) nil)))\n(def tail (lam (l) (l (lam (h t) t) nil)))\n(head (tail (cons a (cons b nil))))", + "answer": "b" + }, + { + "level": 42, + "description": "isNil tests whether a Scott-encoded list is empty. isNil l = l (lam h t -> False) True: a non-empty list immediately calls its cons branch returning False; nil returns its base True. Evaluate (isNil nil).", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def nil (lam (c n) n))\n(def cons (lam (h t c n) (c h t)))\n(def isNil (lam (l) (l (lam (h t) False) True)))\n(isNil nil)", + "answer": "(lam (f t) t)" + }, + { + "level": 43, + "description": "Evaluate (isNil (cons a nil)). A non-empty list is not nil, so the result should be False.", + "expr": "(def False (lam (f t) f))\n(def True (lam (f t) t))\n(def nil (lam (c n) n))\n(def cons (lam (h t c n) (c h t)))\n(def isNil (lam (l) (l (lam (h t) False) True)))\n(isNil (cons a nil))", + "answer": "(lam (f t) f)" + }, + { + "level": 44, + "description": "Church-encoded sum types (Either). Left x = lam l r -> l x tags a value as Left; Right x = lam l r -> r x tags it as Right. either f g e = e f g eliminates the sum by applying the matching handler. Evaluate (either f g (Left a)).", + "expr": "(def Left (lam (x l r) (l x)))\n(def Right (lam (x l r) (r x)))\n(def either (lam (f g e) (e f g)))\n(either f g (Left a))", + "answer": "(f a)" + }, + { + "level": 45, + "description": "Evaluate (either f g (Right a)). The Right handler g should be applied to a.", + "expr": "(def Left (lam (x l r) (l x)))\n(def Right (lam (x l r) (r x)))\n(def either (lam (f g e) (e f g)))\n(either f g (Right a))", + "answer": "(g a)" + }, + { + "level": 46, + "description": "Church-encoded option (Maybe). None = lam n s -> n is the absent case. Some x = lam n s -> s x wraps a value. fromOption default opt = opt default (lam x -> x) returns the wrapped value or the default. Evaluate (fromOption a None).", + "expr": "(def None (lam (n s) n))\n(def Some (lam (x n s) (s x)))\n(def fromOption (lam (default opt) (opt default (lam (x) x))))\n(fromOption a None)", + "answer": "a" + }, + { + "level": 47, + "description": "Evaluate (fromOption a (Some b)). The option contains b, so the default a is ignored and b is returned.", + "expr": "(def None (lam (n s) n))\n(def Some (lam (x n s) (s x)))\n(def fromOption (lam (default opt) (opt default (lam (x) x))))\n(fromOption a (Some b))", + "answer": "b" + }, + { + "level": 48, + "description": "mapOption applies a function inside an Option without unwrapping it. mapOption f opt = opt None (lam x -> Some (f x)): None maps to None; Some x maps to Some (f x). Evaluate (mapOption f (Some a)) and give its fully reduced form.", + "expr": "(def None (lam (n s) n))\n(def Some (lam (x n s) (s x)))\n(def mapOption (lam (f opt) (opt None (lam (x) (Some (f x))))))\n(mapOption f (Some a))", + "answer": "(lam (n s) (s (f a)))" + }, + { + "level": 49, + "description": "The Kleene predecessor uses a pair-stepping trick to compute pred n = n - 1 (with pred zero = zero). Starting from (pair zero zero), each step shifts: (pair (snd p)) (succ (snd p)). After n steps fst of the pair is n-1. Evaluate (pred zero) — it should return zero.", + "expr": "(def zero (lam (s z) z))\n(def one (lam (s z) (s z)))\n(def pair (lam (x y f) (f x y)))\n(def fst (lam (p) (p (lam (x y) x))))\n(def snd (lam (p) (p (lam (x y) y))))\n(def succ (lam (n s z) (s ((n s) z))))\n(def pred (lam (n) (fst (n (lam (p) (pair (snd p) (succ (snd p)))) (pair zero zero)))))\n(pred zero)", + "answer": "(lam (s z) z)" + }, + { + "level": 50, + "description": "Evaluate (pred one) using the same Kleene predecessor. After one pair-step starting from (pair zero zero) the fst is still zero. Confirm that the predecessor of one is zero.", + "expr": "(def zero (lam (s z) z))\n(def one (lam (s z) (s z)))\n(def pair (lam (x y f) (f x y)))\n(def fst (lam (p) (p (lam (x y) x))))\n(def snd (lam (p) (p (lam (x y) y))))\n(def succ (lam (n s z) (s ((n s) z))))\n(def pred (lam (n) (fst (n (lam (p) (pair (snd p) (succ (snd p)))) (pair zero zero)))))\n(pred one)", + "answer": "(lam (s z) z)" + } ] diff --git a/lambda-calcul/haskell/minilang.cabal b/lambda-calcul/haskell/minilang.cabal index d508959..200e5c5 100644 --- a/lambda-calcul/haskell/minilang.cabal +++ b/lambda-calcul/haskell/minilang.cabal @@ -104,7 +104,6 @@ test-suite minilang-test Minilang.REPL.HaskelineSpec Minilang.REPL.NetSpec Minilang.ServerSpec - Exalt.APISpec hs-source-dirs: test default-extensions: diff --git a/lambda-calcul/haskell/plan.md b/lambda-calcul/haskell/plan.md new file mode 100644 index 0000000..2d8a21b --- /dev/null +++ b/lambda-calcul/haskell/plan.md @@ -0,0 +1,552 @@ +# Interpreter Extension Plan + +This document describes a series of extensions to the minilang interpreter, ordered by +increasing difficulty. Each extension is intended to drive new challenges in the contest: +rather than testing knowledge of Church-encoding tricks, these challenges require +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`, + `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`). +- **`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 + (Algorithm W, constraint-based), wired into the REPL but not yet exposed to challenges. +- **`Minilang.REPL.*`** — A layered REPL stack (pure, IO, Haskeline, network) built around + a `MonadREPL` typeclass. +- **`Minilang.App` / `API` / `Server`** — A Servant HTTP server that drives the challenge + contest: register, get challenge, post answer. + +--- + +## 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 + +**Difficulty: 2 / 5** + +### What it is + +Add native integer values to the language. An integer literal like `42` or `-7` is a +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 + +**`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`. + +**`Minilang.Lambda.DeBruijn`** +- Add `FNum Int` to `DeBruijn`, propagated through `toDeBruijn`, `fromDeBruijn`, + `substitute`, `eval`/`eval'`, and `pretty`. + +**`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)`. + +### Example challenges + +| Expression | Result | +|---|---| +| `42` | `42` | +| `(lam (x) x) 99` | `99` | +| `(lam (n) n) -3` | `-3` | + +--- + +## Extension 3 — Built-in arithmetic operators + +**Difficulty: 2 / 5** + +### What it is + +Depends on Extension 2. 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. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Builtin Text Int [Value]` to `Value` (name, remaining arity, accumulated args). +- `eval`: `Var x` where `x` is a known builtin name returns `Builtin x arity []`. +- `apply`: when `f` is `Builtin name 1 args`, dispatch on `name` and reduce; when arity > 1, + return `Builtin name (arity-1) (args ++ [a])`. +- `readBack`: a fully-saturated builtin that wasn't reduced (e.g. `(+ x y)` with free vars) + reads back as a neutral application. + +**`Minilang.Lambda.Parser`** +- Builtin names (`+`, `-`, `*`, `/`, `mod`, `=`, `<`) are already valid identifiers under + the current `extraIdentifierChars` definition, so no parser change is needed beyond + registering them as known names. + +### Example challenges + +| Expression | Result | +|---|---| +| `(+ 3 4)` | `7` | +| `(* 2 (+ 1 4))` | `10` | +| `(- 10 3)` | `7` | +| `(= 3 3)` | `#t` (requires Extension 5) or `True` Church-bool | +| `(+ 1)` | a partial application — prints as a neutral `(+ 1)` | + +--- + +## Extension 4 — String literals + +**Difficulty: 2 / 5** + +### What it is + +Add double-quoted string values. Like integers, strings are self-evaluating. The extra +challenge compared to integers is the round-trip: `pretty` must re-emit surrounding +double-quotes and escape internal special characters, so the parser and printer must agree +on the escape convention. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Str Text` to `Term` and `VStr Text` to `Value`. + +**`Minilang.Lambda.DeBruijn`** +- Add `FStr Text`, propagated everywhere. + +**`Minilang.Lambda.Parser`** +- Add `StrLit Text` to `AST`. +- Parser rule: `char '"' *> manyTill L.charLiteral (char '"')`, tried before `sym`. +- `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=`. + +### Example challenges + +| Expression | Result | +|---|---| +| `"hello"` | `"hello"` | +| `(concat "foo" "bar")` | `"foobar"` | +| `(length "abc")` | `3` | +| `(slice 1 3 "abcde")` | `"bc"` | + +--- + +## Extension 5 — Boolean literals and `if` + +**Difficulty: 2 / 5** + +### What it is + +Add `#t` / `#f` literals and an `if` special form. This is the first form that *cannot* be +desugared into a plain lambda application under call-by-value without Church-encoding, +because `if` must be *non-strict* in its branches to avoid evaluating the untaken one. +A divergent or error-raising expression in the dead branch must not be evaluated. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Bool Bool` to `Term` and `VBool Bool` to `Value`. +- Add `If Term Term Term` to `Term`. +- `eval`: `If cond t e → if evaluate cond then eval env t else eval env e`. Note: only `cond` + is evaluated eagerly; the branches are lazy. + +**`Minilang.Lambda.Parser`** +- Add `BoolLit Bool` and `IfExpr AST AST AST` to `AST`. +- Parser rule for `#t` / `#f`. +- Parser rule for `(if cond then else)` as a special form (not desugared to lambda). +- `desugar`: `IfExpr c t e → If (desugar c) (desugar t) (desugar e)`. + +**`Minilang.Lambda.DeBruijn`** +- Add `FBool Bool` and `DIf` cases, propagated through all functions. + +### Example challenges + +| Expression | Result | +|---|---| +| `#t` | `#t` | +| `(if #t a b)` | `a` | +| `(if #f a b)` | `b` | +| `(if (= 1 1) "yes" "no")` | `"yes"` (requires Extensions 2–4) | +| `(if #f (omega omega) 42)` | `42` — the divergent branch is not evaluated | + +--- + +## Extension 6 — Array literals + +**Difficulty: 3 / 5** + +### What it is + +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. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Arr [Term]` to `Term` and `VArr [Value]` to `Value`. +- `eval`: `Arr es → VArr (map (eval env) es)` — evaluate every element eagerly. +- `readBack`: `VArr vs → Arr (map readBack vs)`. + +**`Minilang.Lambda.DeBruijn`** +- Add `FArr [DeBruijn ann]`, propagated through `toDeBruijn`, `fromDeBruijn`, + `substitute`, `eval`/`eval'`, `pretty`. + +**`Minilang.Lambda.Parser`** +- Add `ArrLit [AST]` to `AST`. +- Parser rule: `between (symbol "[") (symbol "]") (many ast)`. +- `pretty`: `ArrLit es → "[" <> Text.unwords (map pretty es) <> "]"`. + +**Array builtins**: `head`, `tail`, `cons`, `nth`, `length`, `map` (requires lambda values +as arguments — the interaction between array builtins and lambda values is the interesting +new test here). + +### Example challenges + +| Expression | Result | +|---|---| +| `[1 2 3]` | `[1 2 3]` | +| `(head [10 20 30])` | `10` | +| `(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) | + +--- + +## Extension 7 — `quote` and `eval` + +**Difficulty: 3 / 5** + +### What it is + +`(quote e)` (shorthand `'e`) returns the *unevaluated syntax tree* of `e` as a first-class +runtime value — a `VQuote Term`. Evaluation is non-recursive for the quoted sub-expression. +The dual `(eval e)` takes a `VQuote` and re-evaluates it in the current environment, +making the interpreter explicitly two-level. This is the first extension where the +distinction between *object language* and *meta-language* becomes observable in a challenge. + +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. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Quote Term` to `Term` and `VQuote Term` to `Value`. +- `eval`: `Quote t → VQuote t` (does not recurse into `t`). +- `apply`: when `f` is `Builtin "eval" 1 []` and argument is `VQuote t`, call `eval env t`. + This requires `apply` to receive `env` — currently it does not. All call sites of `apply` + must be updated. +- `readBack`: `VQuote t → Quote t` (prints as `'t`). + +**`Minilang.Lambda.Parser`** +- Add `QuoteExpr AST` to `AST`. +- Parser rule for `(quote e)` as a special form. +- Reader macro: `char '\'' *> ast` producing `QuoteExpr`. +- `pretty`: `QuoteExpr e → "(quote " <> pretty e <> ")"` or `"'" <> pretty e`. + +### Example challenges + +| Expression | Result | +|---|---| +| `(quote x)` | `x` (the symbol, not evaluated) | +| `(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) | + +--- + +## Extension 8 — `letrec` / recursive definitions + +**Difficulty: 3 / 5** + +### What it is + +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 +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 +`let rec` in the metalanguage. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Rec Text Term` to `Term` (or handle recursion entirely at the `eval` level without a + new `Term` constructor by building circular `EnvValue` entries using Haskell's laziness). +- `eval`: `Rec f body → let v = eval ((f, v) : env) body in v` (the circular binding). + +**`Minilang.Lambda.Parser`** +- Add `Letrec [(Text, AST)] AST` to `AST`. +- Parser rule for `(letrec ((x e) …) body)` mirroring `letExpr` but desugaring differently. +- `desugar`: translate each binding to a `Rec` node. + +**`Minilang.Lambda.DeBruijn`** +- Add a `Rec` case propagated through all functions. + +### Example challenges + +| Expression | Result | +|---|---| +| `(letrec ((f (lam (x) (if (= x 0) 1 (* x (f (- x 1))))))) (f 5))` | `120` (requires Extensions 3, 5) | +| `(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 + +**Difficulty: 3 / 5** + +### What it is + +Add `ref`, `deref`, and `set!` as built-in operations over a mutable heap. This is the +first extension that introduces *effects* into the otherwise pure evaluator: `eval` can no +longer be a pure function. Its type must change to operate in a state monad (or return a +`(Value, Store)` pair), where `Store` maps fresh location identifiers to current values. +Every call site of `eval` and `apply` must be updated. The interaction between the store and +closures — closures close over variable *bindings*, not store *locations* — makes this a +genuinely instructive design challenge. + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `VRef Int` to `Value` (a reference is a runtime address). +- Add a `Store` type: `IntMap Value`. +- Change `eval :: EnvValue -> Term -> Value` to + `eval :: EnvValue -> Store -> Term -> (Value, Store)` (or use `State Store`). +- `apply` receives and threads `Store`. +- Three new builtins: `ref` (allocate), `deref` (read), `set!` (write and return unit). + +**All call sites** of `eval` and `apply` (in `DeBruijn`, `Lambda`, `REPL.Run`) must be +updated to thread the store. + +### Example challenges + +| Expression | Result | +|---|---| +| `(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) | +| Show that argument evaluation order is observable when both arguments mutate shared state | order-dependent result | + +--- + +## Extension 10 — Type annotations + +**Difficulty: 3 / 5** + +### What it is + +Extends the parser with `(lam ((x : A) …) body)` for annotated binders and `(the T expr)` +for standalone type ascriptions, where `T` is a type expression using `->` and type +variables. The type inferencer already exists; the new challenge is *checking* rather than +*inferring* — when a type annotation is present the inferencer should verify the expression +has exactly that type rather than discovering a fresh one. This is implemented by unifying +the inferred type with the declared type and reporting mismatches. + +### What changes + +**`Minilang.Lambda.Parser`** +- Add a type expression parser: `TyVar Text | TyArr Type Type`, parsed from the same text + syntax as `Unify.Type` already uses (`a`, `b`, `(a -> b)`, etc.). +- Extend the `lambda` parser rule to accept `(x : T)` annotated binders. +- Add a `the` special form: `(the T expr)`. +- Add `Ann Type AST` and `AnnBinder Text Type` constructors to `AST`. + +**`Minilang.Lambda.Infer`** +- `annotate`: when an `Ann` node is encountered, infer the inner expression and then unify + its type with the declared type, returning a `TypeError` if they conflict. +- Annotated binders assign the declared type to the bound variable instead of a fresh type + variable, then check the body against the remaining declared type. + +**`Minilang.Lambda.Eval`** — no change (annotations are erased by `desugar`). + +### Example challenges + +| Expression | Result / type | +|---|---| +| `(the (a -> a) (lam (x) x))` | `(lam (x) x)` | +| `(the (a -> b -> a) (lam (x y) x))` | `(lam (x y) x)` | +| `(the (a -> a -> a) (lam (x y) x))` | unification error: `a` vs `b` | +| `(lam ((x : a) (y : b)) x)` | type `a -> b -> a` | +| `(the (a -> a) (lam (x) (x x)))` | circularity error | + +--- + +## Extension 11 — Algebraic data types + +**Difficulty: 4 / 5** + +### What it is + +Add `(data TypeName (CtorName field …) …)` declarations and `(match expr (pattern body) …)` +expressions. Constructors become first-class values that can be partially applied. +Pattern matching performs structural dispatch and binds sub-components. This is the most +significant structural change to the evaluator so far: it introduces a constructor registry, +a new value form, a pattern-matching engine with backtracking, and a significant expansion +of the type system (sum types, product types, type constructors, arity checking). + +### What changes + +**`Minilang.Lambda.Eval`** +- Add `Con Text [Term]` to `Term` (constructor application) and `VCon Text [Value]` to + `Value`. +- `eval`: `Con name args → VCon name (map (eval env) args)` for saturated constructors; + unsaturated constructors reduce to `Builtin`-style partial values. +- Add `Match Term [(Pattern, Term)]` to `Term`. +- `eval`: `Match scrutinee alts → matchAlts (eval env scrutinee) alts env`, where + `matchAlts` tries each alternative in order, performing structural unification against + `VCon` values, binding matched sub-components, and evaluating the matching branch. + +**`Minilang.Lambda.Parser`** +- Add `DataDecl` and `MatchExpr` to `AST`. +- `data` declarations are processed by a new `runData` step in `loadProgram` that registers + constructors and their arities in the environment. +- Pattern syntax: constructor name (possibly with sub-pattern variables) or wildcard `_`. + +**`Minilang.Lambda.Infer`** +- Add type constructors, sum types, and product types to `Unify.Type`. +- Constructor types are stored in the `Context` alongside term types. +- `infer`: handle `Con` and `Match` nodes; check exhaustiveness (warnings or errors). + +### Example challenges + +| Expression | Result | +|---|---| +| `(data Bool (True) (False)) (match True (True "yes") (False "no"))` | `"yes"` | +| `(data List (Nil) (Cons head tail)) (match (Cons 1 Nil) (Nil 0) ((Cons h t) h))` | `1` | +| `(data Maybe (Nothing) (Just x)) (match (Just 42) (Nothing 0) ((Just v) v))` | `42` | +| Non-exhaustive match | runtime or type error | + +--- + +## Extension 12 — `call/cc` + +**Difficulty: 4 / 5** + +### What it is + +`(call/cc (lam (k) body))` captures the *current continuation* as a first-class value and +passes it to the given function. Invoking `k` with a value immediately returns that value +from the enclosing `call/cc`, discarding the rest of the computation. This is the most +fundamental control-flow extension: it can encode exceptions, early exit, cooperative +multitasking, and backtracking. Implementing it correctly requires transforming `eval` +into *continuation-passing style* — either explicitly by changing the return type to +`(Value -> r) -> r`, or by using a `Cont` monad. Either way every call site changes. + +### What changes + +**`Minilang.Lambda.Eval`** +- Change `eval` signature from `EnvValue -> Term -> Value` to + `EnvValue -> Term -> (Value -> r) -> r` (or `EnvValue -> Term -> Cont r Value`). +- `apply` receives the current continuation as an extra argument. +- Add `VCont (Value -> r)` to `Value` (a captured continuation). +- `apply` on a `VCont k v`: simply call `k v`, discarding everything after the current + continuation — this is the "abort to the capture point" behaviour. +- `eval` for `App f a` in CPS: evaluate `f`, evaluate `a`, then `apply f' a' k`. +- Register `call/cc` as a known name; `eval` of `Var "call/cc"` returns a `VBuiltin` that, + when applied to a function `f`, calls `f` with `VCont k` where `k` is the current + continuation. + +**All call sites** of `eval` (in `DeBruijn`, `Lambda`, `REPL.Run`, `App`) must be updated +to supply an initial continuation (typically `id`). + +**`Minilang.Lambda.Parser`** — no change; `call/cc` is a valid identifier already. + +### Example challenges + +| Expression | Result | +|---|---| +| `(call/cc (lam (k) 42))` | `42` (k never used) | +| `(call/cc (lam (k) (k 42) 99))` | `42` (early return, 99 is never reached) | +| `(+ 1 (call/cc (lam (k) (* 2 (k 3)))))` | `4` | +| Implement `throw`/`catch` using `call/cc` | | +| Implement list collection with early termination | | + +--- + +## Extension 13 — Delimited continuations (`reset` / `shift`) + +**Difficulty: 5 / 5** + +### What it is + +A refinement of `call/cc` (#12) where continuations are *delimited*: `(shift k body)` +captures only the continuation up to the nearest enclosing `(reset expr)` boundary, rather +than the entire rest of the program. The captured continuation `k` is a *composable +function*, not an escape: calling it does not abort but resumes. This is the basis for +algebraic effects, generators, coroutines, and non-determinism, all expressible without any +further language changes. + +Implementing this correctly requires moving from a flat CPS transform (one continuation +argument) to a *two-level* architecture: an *outer* continuation representing the program +after the current `reset`, and an *inner* continuation representing the program up to the +`reset`. Danvy & Filinski's original presentation encodes this with a two-argument CPS +transform; alternatively, an explicit *continuation stack with reset marks* can be +maintained as a mutable data structure threaded through `eval`. + +### What changes + +**`Minilang.Lambda.Eval`** +- Prerequisite: Extension 12 (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 + continuation; when `expr` completes normally, pass its value to the outer continuation. +- `shift k body`: capture the current inner continuation as a composable function `k`, + install the outer continuation as the new current continuation, and evaluate `body`. +- Add `VShift` and `VReset` administrative value forms (used during evaluation, not + user-visible). + +**`Minilang.Lambda.Parser`** — add `reset` and `shift` as special forms. + +### Example challenges + +| Expression | Result | +|---|---| +| `(reset (+ 1 (shift k 10)))` | `10` (k discarded) | +| `(reset (+ 1 (shift k (k 10))))` | `11` (k applied once: adds 1) | +| `(reset (+ 1 (shift k (k (k 10)))))` | `12` (k applied twice) | +| Implement a generator using `shift`/`reset` | sequence of yielded values | +| Implement `amb` for non-deterministic choice | list of all results | +| Implement a cooperative coroutine scheduler | interleaved output | diff --git a/lambda-calcul/haskell/src/Minilang/API.hs b/lambda-calcul/haskell/src/Minilang/API.hs index 43baddf..0be70ff 100644 --- a/lambda-calcul/haskell/src/Minilang/API.hs +++ b/lambda-calcul/haskell/src/Minilang/API.hs @@ -131,13 +131,15 @@ newToken = first LBS.pack . uniformList 16 data Challenge = Challenge { level :: Int, - expr :: Text + expr :: Text, + description :: Text, + answer :: Text } deriving (Eq, Show, Generic, ToJSON, FromJSON) defaultChallenges :: [Challenge] defaultChallenges = - [ Challenge 0 "x", - Challenge 1 "y", - Challenge 2 "(lam (x) x)" + [ Challenge 0 "x" "A lone free variable. What does x reduce to?" "x", + Challenge 1 "y" "Another free variable. What does y reduce to?" "y", + Challenge 2 "(lam (x) x)" "The identity function. What is its normal form?" "(lam (x) x)" ] diff --git a/lambda-calcul/haskell/src/Minilang/App.hs b/lambda-calcul/haskell/src/Minilang/App.hs index 915f264..cce48f7 100644 --- a/lambda-calcul/haskell/src/Minilang/App.hs +++ b/lambda-calcul/haskell/src/Minilang/App.hs @@ -151,11 +151,11 @@ postAnswer (Just token) expected = do result = evaluateOutputs outputs expected updateUserLastTest token result case result of - TestSucceeded -> do + TestSucceeded -> upgradeUserChallenge token TestFailed msg -> liftIO $ throwM $ err400 {errBody = "Test failed: " <> LBS.fromStrict (encodeUtf8 msg)} - TestErrored msg -> do + TestErrored msg -> liftIO $ throwM $ err500 {errBody = "Error evaluating answer: " <> LBS.fromStrict (encodeUtf8 msg)} data TestResult = TestSucceeded | TestFailed Text | TestErrored Text @@ -167,7 +167,7 @@ isSuccess _ = False evaluateOutputs :: [Out] -> Text -> TestResult evaluateOutputs outputs expected = case outputs of - [Bye, Evaluated ast _ _] -> do + [Bye, Evaluated ast _ _] -> if pretty ast /= expected then TestFailed "Incorrect result" else TestSucceeded diff --git a/lambda-calcul/haskell/test/Minilang/ServerSpec.hs b/lambda-calcul/haskell/test/Minilang/ServerSpec.hs index 80e9f5e..f61969a 100644 --- a/lambda-calcul/haskell/test/Minilang/ServerSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/ServerSpec.hs @@ -83,7 +83,7 @@ spec = with (app testSeed) $ do `shouldRespondWith` 404 it "GET /api/challenge returns next challenge given user is registered" $ do - let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge {level = 0, expr = "x"} + let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge {level = 0, expr = "x", description = "A lone free variable. What does x reduce to?", answer = "x"} postJSON "/api/register" alice `shouldRespondWith` 201 @@ -122,7 +122,7 @@ spec = with (app testSeed) $ do `shouldRespondWith` 400 it "GET /api/challenge returns next level challenge after successful POST" $ do - let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge {level = 1, expr = "y"} + let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge {level = 1, expr = "y", description = "Another free variable. What does y reduce to?", answer = "y"} void $ postJSON "/api/register" alice void $ postJSON ("/api/challenge?token=" <> LBS.toStrict token) "\"x\"" |