Add more challenges and plans for enhancement of the interpreter

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\""