Add integers parsing

6 files changed, 273 insertions, 112 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
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
index 025fd39..1e85ca6 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -4,12 +4,13 @@ module Minilang.Lambda.DeBruijn where
 
 import Data.List (elemIndex)
 import Data.Text (Text)
+import qualified Data.Text
 import Minilang.Lambda.Eval (Term)
 import qualified Minilang.Lambda.Eval as Eval
-import Debug.Trace (trace)
 
 data DeBruijn ann
   = FV Text
+  | FNum Int
   | Var ann Int
   | Lam ann (DeBruijn ann)
   | App (DeBruijn ann) (DeBruijn ann)
@@ -23,6 +24,7 @@ newEnv = []
 fromDeBruijn :: DeBruijn Text -> Term
 fromDeBruijn = \case
   FV x -> Eval.Var x
+  FNum n -> Eval.Num n
   Var s _ -> Eval.Var s
   Lam s body -> Eval.Lam s (fromDeBruijn body)
   App f a -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
@@ -39,6 +41,8 @@ toDeBruijn term = go term []
       Lam x (go body (x : env))
     go (Eval.App f a) env =
       App (go f env) (go a env)
+    go (Eval.Num n) _env =
+      FNum n
 
 eval :: DeBruijn ann -> DeBruijn ann
 eval (App f a) =
@@ -64,6 +68,7 @@ substitute env n arg term = case term of
   FV x -> case lookup x env of
     Just term -> term
     Nothing -> FV x
+  FNum _ -> term
   Var t x
     | x == n -> arg
     | otherwise -> Var t x
@@ -73,6 +78,13 @@ substitute env n arg term = case term of
 pretty :: DeBruijn Text -> Text
 pretty = \case
   FV x -> x
+  FNum n -> showNum n
   Var s _ -> s
   Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
   App f a -> "(" <> pretty f <> " " <> pretty a <> ")"
+
+-- | Render an integer, using no space between '-' and digits for negative numbers.
+showNum :: Int -> Text
+showNum n
+  | n < 0     = "-" <> Data.Text.pack (show (abs n))
+  | otherwise = Data.Text.pack (show n)
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index e5530eb..650c4bd 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -12,15 +12,16 @@ data Term
   = Var Text
   | Lam Text Term
   | App Term Term
+  | Num Int
   deriving (Show, Read, Eq, Generic, ToJSON, FromJSON)
 
 instance IsString Term where
   fromString = Var . pack
 
-data Value = Clos EnvValue Text Term | VNeut Neutral
+data Value = Clos EnvValue Text Term | VNeut Neutral | VNum Int
   deriving (Show, Read, Eq)
 
-data Neutral = NVar Text | NApp Neutral Value
+data Neutral = NVar Text | NNum Int | NApp Neutral Value
   deriving (Show, Read, Eq)
 
 type Env = [(Text, Term)]
@@ -45,6 +46,7 @@ eval env = \case
     let f' = eval env f
         a' = eval env a
      in f' `seq` a' `seq` apply f' a'
+  Num n -> VNum n
 
 apply :: Value -> Value -> Value
 apply f a =
@@ -53,6 +55,7 @@ apply f a =
       let env' = (x, a) : closureEnv
        in eval env' body
     VNeut f' -> VNeut (NApp f' a)
+    VNum n -> VNeut (NApp (NNum n) a)
 
 readBack :: Value -> Term
 readBack = go []
@@ -64,7 +67,9 @@ readBack = go []
             val' = eval ((x, VNeut (NVar name)) : env) body
          in Lam name (go names' val')
       VNeut (NVar n) -> Var n
+      VNeut (NNum n) -> Num n
       VNeut (NApp f a) -> App (go names (VNeut f)) (go names a)
+      VNum n -> Num n
 
 freshName :: Text -> [Text] -> Text
 freshName x names
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
index a0cc577..bf92daa 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
@@ -14,8 +14,8 @@ import Data.Void (Void)
 import GHC.Generics (Generic)
 import Minilang.Lambda.Eval (Term)
 import qualified Minilang.Lambda.Eval as Eval
-import Text.Megaparsec (Parsec, between, empty, errorBundlePretty, parse, some, try)
-import Text.Megaparsec.Char (alphaNumChar, char, letterChar, space1, symbolChar)
+import Text.Megaparsec (Parsec, between, empty, errorBundlePretty, optional, parse, some, try)
+import Text.Megaparsec.Char (alphaNumChar, char, digitChar, letterChar, space1, symbolChar)
 import qualified Text.Megaparsec.Char.Lexer as L
 
 type Parser = Parsec Void Text
@@ -25,6 +25,7 @@ data ParseError = ParseError Text
 
 data AST
   = Sym Text
+  | Lit Int
   | Abs [Text] AST
   | App AST AST [AST]
   | Def Text AST
@@ -33,6 +34,7 @@ data AST
 desugar :: AST -> Term
 desugar = \case
   Sym symb -> Eval.Var symb
+  Lit n -> Eval.Num n
   Abs bound body ->
     foldr
       Eval.Lam
@@ -49,6 +51,7 @@ desugar = \case
 resugar :: Term -> AST
 resugar = \case
   Eval.Var s -> Sym s
+  Eval.Num n -> Lit n
   Eval.Lam x body -> case resugar body of
     Abs vars ast -> Abs (x : vars) ast
     other -> Abs [x] other
@@ -63,10 +66,17 @@ resugar = \case
 pretty :: AST -> Text
 pretty = \case
   Sym symb -> symb
+  Lit n -> prettyInt n
   Abs bound body -> "(lam (" <> Text.unwords bound <> ") " <> pretty body <> ")"
   App x y rest -> "(" <> mconcat (List.intersperse " " (pretty <$> (x : y : rest))) <> ")"
   Def name body -> "(def " <> name <> " " <> pretty body <> ")"
 
+-- | Render an integer with no space between '-' and digits for negative numbers.
+prettyInt :: Int -> Text
+prettyInt n
+  | n < 0     = "-" <> Text.pack (show (abs n))
+  | otherwise = Text.pack (show n)
+
 parseProgram :: Text -> Either ParseError [AST]
 parseProgram input =
   first (ParseError . pack . errorBundlePretty) $
@@ -77,7 +87,7 @@ parse =
   first (ParseError . pack . errorBundlePretty) . Text.Megaparsec.parse ast ""
 
 ast :: Parser AST
-ast = try defExpr <|> try letExpr <|> try lambda <|> try sym <|> try app
+ast = try defExpr <|> try letExpr <|> try lambda <|> try lit <|> try sym <|> try app
 
 app :: Parser AST
 app =
@@ -141,6 +151,18 @@ rpar = symbol ")"
 symbol :: Text -> Parser Text
 symbol = L.symbol spaceConsumer
 
+-- | Parse an integer literal.  The minus sign, if present, must immediately
+-- precede the digits with no intervening whitespace; this distinguishes @-7@
+-- (a negative number) from @- 7@ (the identifier @-@ applied to @7@).
+lit :: Parser AST
+lit = lexeme $ do
+  sign <- optional (char '-')
+  digits <- some digitChar
+  let n = read digits
+  pure $ Lit $ case sign of
+    Just _  -> negate n
+    Nothing -> n
+
 sym :: Parser AST
 sym = Sym . pack <$> identifier
 
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index d772fe0..f07b5a2 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -2,8 +2,11 @@ module Minilang.Lambda.EvalSpec (spec) where
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.Async (race_)
-import Minilang.Lambda.Eval (Term (..), Value, eval, normalise)
-import Test.Hspec (Spec, describe, it, pending, shouldBe)
+import Minilang.Lambda.Eval (Term (..), Value (..), eval, normalise)
+import Test.Hspec (Spec, describe, it, shouldBe)
+import Test.Hspec.QuickCheck (prop)
+import Data.Text (pack)
+import Test.QuickCheck (NonEmptyList (..), arbitrary, forAll, (===))
 
 spec :: Spec
 spec = do
@@ -65,6 +68,25 @@ spec = do
       normalise (App (App add' one) one)
         `shouldBe` two
 
+  describe "integer literals" $ do
+    -- An integer literal is already a normal form: normalise must return it unchanged.
+    prop "any integer literal normalises to itself" $ \n ->
+      normalise (Num n) === Num (n :: Int)
+
+    -- eval on a bare Num must always produce the VNum value form, never a closure
+    -- or neutral, regardless of the integer's sign or magnitude.
+    prop "eval of any integer literal produces VNum" $ \n ->
+      eval [] (Num n) === VNum (n :: Int)
+
+    -- A number is not a function.  Applying it to any argument must leave a stuck
+    -- neutral application: App (Num n) (normalise arg).  We test this with free
+    -- variables as arguments, which are themselves already in normal form.
+    prop "an integer in function position produces a stuck application" $
+      forAll arbitrary $ \n ->
+        forAll (getNonEmpty <$> arbitrary) $ \x ->
+          normalise (App (Num n) (Var (pack x)))
+            === App (Num (n :: Int)) (Var (pack x))
+
   -- describe "call-by-name eval" $ do
   --   it "evaluates 'x' as itself" $ do
   --     normalise' (Var "x") `shouldBe` Var "x"
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
index 932eff6..e9cfc6b 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
@@ -4,31 +4,33 @@
 
 module Minilang.Lambda.ParserSpec where
 
-import Data.Either (isRight)
+import Data.Either (isLeft, isRight)
 import Data.Function ((&))
 import Data.Text (Text, pack)
 import qualified Data.Text as Text
 import Minilang.Lambda.Eval (Term (Lam))
 import qualified Minilang.Lambda.Eval as Eval
 import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars)
-import Test.Hspec (Spec, it, parallel, shouldBe, shouldSatisfy)
+import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy)
 import Test.Hspec.QuickCheck (prop)
-import Test.QuickCheck
-  ( Arbitrary (..),
-    Gen,
-    NonEmptyList (..),
-    counterexample,
-    elements,
-    forAll,
-    forAllShrink,
-    listOf,
-    oneof,
-    resize,
-    sized,
-    vectorOf,
-    (===),
-    (==>),
-  )
+import Test.QuickCheck (
+  Arbitrary (..),
+  Gen,
+  NonEmptyList (..),
+  Positive (..),
+  counterexample,
+  elements,
+  forAll,
+  forAllShrink,
+  listOf,
+  oneof,
+  resize,
+  sized,
+  suchThat,
+  vectorOf,
+  (===),
+  (==>),
+ )
 
 -- ((f x) y) --> (f x y)
 -- (lam (x) (lam (y) y)) --> (lam (x y) y)
@@ -103,6 +105,15 @@ spec = parallel $ do
       let text = pretty ast
        in parse text `shouldBe` Right ast
 
+  describe "integer literals" $ do
+    prop "any integer rendered by pretty parses back to the same Lit" $ \n ->
+      parse (pretty (Lit n)) === Right (Lit (n :: Int))
+
+    prop "a '-' separated from digits by spaces does not parse as an integer literal" $
+      forAll (getPositive <$> (arbitrary :: Gen (Positive Int))) $ \n ->
+        let spaced = "- " <> Text.pack (show n)
+         in parse spaced `shouldSatisfy` (/= Right (Lit (negate n)))
+
   it "parses multiline program with blank lines" $ do
     let program =
           "(def id (lam (x) x))\n\
@@ -111,10 +122,10 @@ spec = parallel $ do
           \(def apply (lam (f x) (f x)))\n\
           \(apply id const)"
         expected =
-          [ Def "id" (Abs ["x"] (Sym "x")),
-            Def "const" (Abs ["x", "y"] (Sym "x")),
-            Def "apply" (Abs ["f", "x"] (App (Sym "f") (Sym "x") [])),
-            App
+          [ Def "id" (Abs ["x"] (Sym "x"))
+          , Def "const" (Abs ["x", "y"] (Sym "x"))
+          , Def "apply" (Abs ["f", "x"] (App (Sym "f") (Sym "x") []))
+          , App
               (Sym "apply")
               (Sym "id")
               [Sym "const"]
@@ -136,35 +147,50 @@ newtype Identifier = Identifier {unIdent :: Text}
 
 instance Arbitrary Identifier where
   arbitrary =
-    Identifier . pack
-      <$> ((:) <$> elements initialChars <*> listOf (elements restChars))
+    ( Identifier . pack
+        <$> ((:) <$> elements initialChars <*> listOf (elements restChars))
+    )
+      `suchThat` (not . isIntLiteral . unIdent)
+   where
+    -- An identifier whose first characters would be consumed as an integer
+    -- literal by the parser must be excluded: the parser tries `lit` before
+    -- `sym`, so any string starting with digits, or with '-' immediately
+    -- followed by digits, would produce a Lit rather than a Sym.
+    isIntLiteral t =
+      case Text.unpack t of
+        ('-' : d : _) -> isDigit d
+        (d : _) -> isDigit d
+        [] -> False
+    isDigit c = c >= '0' && c <= '9'
 
 instance Arbitrary AST where
   arbitrary = genAst 10
 
   shrink = \case
     Sym _ -> []
+    Lit _ -> []
     Abs bind body -> case shrink (Identifier <$> bind) of
       [] -> shrink body
       bind' ->
         [ shrunkAbs (unIdent <$> bound) body'
-          | bound <- bind',
-            body' <- shrink body
+        | bound <- bind'
+        , body' <- shrink body
         ]
-        where
-          shrunkAbs [] b = b
-          shrunkAbs bound b = Abs bound b
+       where
+        shrunkAbs [] b = b
+        shrunkAbs bound b = Abs bound b
     App x y [] -> [x, y]
     App x y rest -> (App x y <$> shrink rest) <> [x, y]
     Def _name body -> shrink body -- never generated
 
 genAst :: Int -> Gen AST
-genAst 0 = Sym . unIdent <$> arbitrary
+genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary]
 genAst depth =
   oneof
-    [ Sym . unIdent <$> arbitrary,
-      genAbstraction depth,
-      genApplication depth
+    [ Sym . unIdent <$> arbitrary
+    , Lit <$> arbitrary
+    , genAbstraction depth
+    , genApplication depth
     ]
 
 genDef :: Int -> Gen AST
@@ -173,8 +199,8 @@ genDef n = Def . unIdent <$> arbitrary <*> genAst n
 genApplication :: Int -> Gen AST
 genApplication depth = do
   App <$> genAst d <*> genAst d <*> reasonablySized (listOf $ genAst d)
-  where
-    d = depth - 1
+ where
+  d = depth - 1
 
 genAbstraction :: Int -> Gen AST
 genAbstraction depth = do