Add strings handling

9 files changed, 542 insertions, 72 deletions

diff --git a/lambda-calcul/haskell/challenges.json b/lambda-calcul/haskell/challenges.json
index 75561c5..16d2f48 100644
--- a/lambda-calcul/haskell/challenges.json
+++ b/lambda-calcul/haskell/challenges.json
@@ -169,312 +169,462 @@
   },
   {
     "level": 28,
+    "description": "String literals are double-quoted values that self-evaluate \u2014 they need no reduction. What does \"hello\" reduce to?",
+    "expr": "\"hello\"",
+    "answer": "\"hello\""
+  },
+  {
+    "level": 29,
+    "description": "Strings can contain spaces and any printable character. What does \"foo bar\" reduce to?",
+    "expr": "\"foo bar\"",
+    "answer": "\"foo bar\""
+  },
+  {
+    "level": 30,
+    "description": "Apply the identity function to a string literal. What does ((lam (x) x) \"world\") reduce to?",
+    "expr": "((lam (x) x) \"world\")",
+    "answer": "\"world\""
+  },
+  {
+    "level": 31,
+    "description": "str-concat takes two strings and concatenates them. What does (str-concat \"foo\" \"bar\") reduce to?",
+    "expr": "(str-concat \"foo\" \"bar\")",
+    "answer": "\"foobar\""
+  },
+  {
+    "level": 32,
+    "description": "str-concat can be nested. What does (str-concat \"hello\" (str-concat \" \" \"world\")) reduce to?",
+    "expr": "(str-concat \"hello\" (str-concat \" \" \"world\"))",
+    "answer": "\"hello world\""
+  },
+  {
+    "level": 33,
+    "description": "str-length takes a string and returns its length as an integer. What does (str-length \"hello\") reduce to?",
+    "expr": "(str-length \"hello\")",
+    "answer": "5"
+  },
+  {
+    "level": 34,
+    "description": "What does (str-length \"\") reduce to? The empty string has length zero.",
+    "expr": "(str-length \"\")",
+    "answer": "0"
+  },
+  {
+    "level": 35,
+    "description": "str-slice takes a start index (inclusive), an end index (exclusive), and a string, and returns the sub-string. What does (str-slice 0 3 \"abcde\") reduce to?",
+    "expr": "(str-slice 0 3 \"abcde\")",
+    "answer": "\"abc\""
+  },
+  {
+    "level": 36,
+    "description": "What does (str-slice 1 4 \"abcde\") reduce to? Characters at indices 1, 2, and 3 are selected.",
+    "expr": "(str-slice 1 4 \"abcde\")",
+    "answer": "\"bcd\""
+  },
+  {
+    "level": 37,
+    "description": "str= takes two strings and returns the Church boolean True (lam (f t) t) if they are equal, False (lam (f t) f) otherwise. What does (str= \"abc\" \"abc\") reduce to?",
+    "expr": "(str= \"abc\" \"abc\")",
+    "answer": "(lam (f t) t)"
+  },
+  {
+    "level": 38,
+    "description": "What does (str= \"abc\" \"xyz\") reduce to? The strings are not equal.",
+    "expr": "(str= \"abc\" \"xyz\")",
+    "answer": "(lam (f t) f)"
+  },
+  {
+    "level": 39,
+    "description": "str< returns Church True when its first argument is lexicographically less than its second. What does (str< \"apple\" \"banana\") reduce to?",
+    "expr": "(str< \"apple\" \"banana\")",
+    "answer": "(lam (f t) t)"
+  },
+  {
+    "level": 40,
+    "description": "What does (str< \"z\" \"a\") reduce to? \"z\" is not less than \"a\" lexicographically.",
+    "expr": "(str< \"z\" \"a\")",
+    "answer": "(lam (f t) f)"
+  },
+  {
+    "level": 41,
+    "description": "Like arithmetic operators, string builtins support partial application. Applying str-concat to one argument produces a function waiting for its second. What does (str-concat \"hello\") reduce to?",
+    "expr": "(str-concat \"hello\")",
+    "answer": "(str-concat \"hello\")"
+  },
+  {
+    "level": 42,
+    "description": "When a string builtin receives a free variable as an argument it cannot reduce and stays stuck. What does (str-concat x \"bar\") reduce to?",
+    "expr": "(str-concat x \"bar\")",
+    "answer": "(str-concat x \"bar\")"
+  },
+  {
+    "level": 43,
+    "description": "Use def to bind a string, then apply str-length to it. What does (str-length greeting) produce in this program?",
+    "expr": "(def greeting \"hello\")\n(str-length greeting)",
+    "answer": "5"
+  },
+  {
+    "level": 44,
+    "description": "Use let to bind a string and then concatenate it with another string. What does (let ((s \"hello\")) (str-concat s \"!\")) reduce to?",
+    "expr": "(let ((s \"hello\")) (str-concat s \"!\"))",
+    "answer": "\"hello!\""
+  },
+  {
+    "level": 45,
+    "description": "String builtins are first-class values and can be passed as arguments to lambdas. What does ((lam (f) (f \"hello\" \" world\")) str-concat) reduce to?",
+    "expr": "((lam (f) (f \"hello\" \" world\")) str-concat)",
+    "answer": "\"hello world\""
+  },
+  {
+    "level": 46,
+    "description": "A string literal can contain any character, including parentheses. The parser recognises ( and ) as delimiters only outside a string. What does \"(hello)\" reduce to?",
+    "expr": "\"(hello)\"",
+    "answer": "\"(hello)\""
+  },
+  {
+    "level": 47,
+    "description": "A string can contain only an opening parenthesis with no closing match \u2014 the parser does not need to see balanced parens inside a string. What does \"(\" reduce to?",
+    "expr": "\"(\"",
+    "answer": "\"(\""
+  },
+  {
+    "level": 48,
+    "description": "Likewise a string can start with a closing parenthesis. What does \")\" reduce to?",
+    "expr": "\")\"",
+    "answer": "\")\""
+  },
+  {
+    "level": 49,
+    "description": "A string that looks exactly like a lambda expression is still just a string \u2014 it is not evaluated. What does \"(lam (x) x)\" reduce to?",
+    "expr": "\"(lam (x) x)\"",
+    "answer": "\"(lam (x) x)\""
+  },
+  {
+    "level": 50,
+    "description": "Use str-concat to join two paren strings. The result is a correctly balanced parenthesis pair as a string value. What does (str-concat \"(\" \")\") reduce to?",
+    "expr": "(str-concat \"(\" \")\")",
+    "answer": "\"()\""
+  },
+  {
+    "level": 51,
+    "description": "str-length counts every character including parentheses. What does (str-length \"(hello)\") reduce to?",
+    "expr": "(str-length \"(hello)\")",
+    "answer": "7"
+  },
+  {
+    "level": 52,
+    "description": "str-slice works on strings containing parentheses just like any other string. What does (str-slice 0 3 \"(ab)\") reduce to?",
+    "expr": "(str-slice 0 3 \"(ab)\")",
+    "answer": "\"(ab\""
+  },
+  {
+    "level": 53,
     "description": "The interpreter now has built-in arithmetic operators. + takes two integers and returns their sum. What does (+ 3 4) reduce to?",
     "expr": "(+ 3 4)",
     "answer": "7"
   },
   {
-    "level": 29,
+    "level": 54,
     "description": "The built-in - subtracts its second argument from its first. What does (- 10 3) reduce to?",
     "expr": "(- 10 3)",
     "answer": "7"
   },
   {
-    "level": 30,
+    "level": 55,
     "description": "The built-in * multiplies two integers. What does (* 6 7) reduce to?",
     "expr": "(* 6 7)",
     "answer": "42"
   },
   {
-    "level": 31,
+    "level": 56,
     "description": "div performs integer division (truncated toward negative infinity). What does (div 17 5) reduce to?",
     "expr": "(div 17 5)",
     "answer": "3"
   },
   {
-    "level": 32,
+    "level": 57,
     "description": "mod returns the remainder of integer division. What does (mod 17 5) reduce to?",
     "expr": "(mod 17 5)",
     "answer": "2"
   },
   {
-    "level": 33,
+    "level": 58,
     "description": "neg is a unary built-in that negates its argument. What does (neg 5) reduce to?",
     "expr": "(neg 5)",
     "answer": "-5"
   },
   {
-    "level": 34,
+    "level": 59,
     "description": "Built-ins compose freely. * and + can be nested just like lambda applications. What does (* 2 (+ 3 4)) reduce to?",
     "expr": "(* 2 (+ 3 4))",
     "answer": "14"
   },
   {
-    "level": 35,
+    "level": 60,
     "description": "Pythagorean-style expression: (+ (* 3 3) (* 4 4)) computes 9 + 16. What is the result?",
     "expr": "(+ (* 3 3) (* 4 4))",
     "answer": "25"
   },
   {
-    "level": 36,
+    "level": 61,
     "description": "= is a built-in equality test. It returns the Church boolean True (lam (f t) t) when both arguments are equal and False (lam (f t) f) otherwise. What does (= 42 42) reduce to?",
     "expr": "(= 42 42)",
     "answer": "(lam (f t) t)"
   },
   {
-    "level": 37,
+    "level": 62,
     "description": "What does (= 42 0) reduce to? The two integers are not equal, so = returns the Church boolean False.",
     "expr": "(= 42 0)",
     "answer": "(lam (f t) f)"
   },
   {
-    "level": 38,
+    "level": 63,
     "description": "< is a built-in less-than test. It returns the Church boolean True when the first argument is strictly less than the second, False otherwise. What does (< 3 5) reduce to?",
     "expr": "(< 3 5)",
     "answer": "(lam (f t) t)"
   },
   {
-    "level": 39,
+    "level": 64,
     "description": "What does (< 5 3) reduce to? 5 is not less than 3, so < returns the Church boolean False.",
     "expr": "(< 5 3)",
     "answer": "(lam (f t) f)"
   },
   {
-    "level": 40,
+    "level": 65,
     "description": "Built-ins support partial application just like lambdas. Applying + to only one argument produces a function waiting for its second argument. What does (+ 1) reduce to?",
     "expr": "(+ 1)",
     "answer": "(+ 1)"
   },
   {
-    "level": 41,
+    "level": 66,
     "description": "A partially applied built-in is a first-class value that can be passed to and invoked by a lambda. What does ((lam (f) (f 10)) (+ 5)) reduce to?",
     "expr": "((lam (f) (f 10)) (+ 5))",
     "answer": "15"
   },
   {
-    "level": 42,
+    "level": 67,
     "description": "When a built-in operator receives a free variable as one of its arguments it cannot reduce and stays as a stuck neutral term. What does (+ x 1) reduce to?",
     "expr": "(+ x 1)",
     "answer": "(+ x 1)"
   },
   {
-    "level": 43,
+    "level": 68,
     "description": "Division by zero cannot be reduced \u2014 it stays as a stuck neutral application. What does (div 7 0) reduce to?",
     "expr": "(div 7 0)",
     "answer": "(div 7 0)"
   },
   {
-    "level": 44,
+    "level": 69,
     "description": "Use def to bind a lambda that uses * to square its argument, then apply it. What does (square 9) produce in this program?",
     "expr": "(def square (lam (x) (* x x)))\n(square 9)",
     "answer": "81"
   },
   {
-    "level": 45,
+    "level": 70,
     "description": "Use let to bind two integers and compute the sum of their squares. What does (let ((x 3) (y 4)) (+ (* x x) (* y y))) reduce to?",
     "expr": "(let ((x 3) (y 4)) (+ (* x x) (* y y)))",
     "answer": "25"
   },
   {
-    "level": 46,
+    "level": 71,
     "description": "Built-in operators are first-class values: they can be passed as arguments to lambdas. Here a lambda takes an operator f and two arguments x y and applies (f x y). What does ((lam (f x y) (f x y)) + 10 20) reduce to?",
     "expr": "((lam (f x y) (f x y)) + 10 20)",
     "answer": "30"
   },
   {
-    "level": 47,
+    "level": 72,
     "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": 48,
+    "level": 73,
     "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": 49,
+    "level": 74,
     "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": 50,
+    "level": 75,
     "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": 51,
+    "level": 76,
     "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) \u2014 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": 52,
+    "level": 77,
     "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": 53,
+    "level": 78,
     "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": 54,
+    "level": 79,
     "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": 55,
+    "level": 80,
     "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": 56,
+    "level": 81,
     "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": 57,
+    "level": 82,
     "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": 58,
+    "level": 83,
     "description": "two = lam s z -> s (s z) applies s twice. Evaluate (two f x) \u2014 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": 59,
+    "level": 84,
     "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": 60,
+    "level": 85,
     "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": 61,
+    "level": 86,
     "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": 62,
+    "level": 87,
     "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": 63,
+    "level": 88,
     "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": 64,
+    "level": 89,
     "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) \u2014 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": 65,
+    "level": 90,
     "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": 66,
+    "level": 91,
     "description": "The B combinator (composition): B f g x = f (g x). It is function composition. Evaluate (B f g x) \u2014 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": 67,
+    "level": 92,
     "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": 68,
+    "level": 93,
     "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": 69,
+    "level": 94,
     "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": 70,
+    "level": 95,
     "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)))) \u2014 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": 71,
+    "level": 96,
     "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": 72,
+    "level": 97,
     "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": 73,
+    "level": 98,
     "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": 74,
+    "level": 99,
     "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": 75,
+    "level": 100,
     "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": 76,
+    "level": 101,
     "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": 77,
+    "level": 102,
     "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": 78,
+    "level": 103,
     "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) \u2014 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": 79,
+    "level": 104,
     "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/plan.md b/lambda-calcul/haskell/plan.md
index 7c5627e..f7d545f 100644
--- a/lambda-calcul/haskell/plan.md
+++ b/lambda-calcul/haskell/plan.md
@@ -77,7 +77,7 @@ self-evaluating value — it needs no reduction. This is the smallest possible e
 
 ---
 
-## Extension 2 — Built-in arithmetic operators
+## Extension 2 — Built-in arithmetic operators ✅ implemented
 
 **Difficulty: 2 / 5**
 
@@ -115,7 +115,7 @@ rather than an error.
 
 ---
 
-## Extension 3 — String literals
+## Extension 3 — String literals ✅ implemented
 
 **Difficulty: 2 / 5**
 
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
index 1d2f9e8..d3c14e3 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -5,13 +5,14 @@ module Minilang.Lambda.DeBruijn where
 import Data.List (elemIndex)
 import qualified Data.Map.Strict as Map
 import Data.Text (Text)
-import qualified Data.Text
+import qualified Data.Text as Text
 import Minilang.Lambda.Eval (Term)
 import qualified Minilang.Lambda.Eval as Eval
 
 data DeBruijn ann
   = FV Text
   | FNum Int
+  | FStr Text              -- ^ a string literal (closed value)
   | FBuiltin Text          -- ^ a fully-applied or partial built-in operator
   | Var ann Int
   | Lam ann (DeBruijn ann)
@@ -34,6 +35,7 @@ fromDeBruijn :: DeBruijn Text -> Term
 fromDeBruijn = \case
   FV x        -> Eval.Var x
   FNum n      -> Eval.Num n
+  FStr s      -> Eval.Str s
   FBuiltin b  -> Eval.Var b        -- reads back as a Var; eval recognises it
   Var s _     -> Eval.Var s
   Lam s body  -> Eval.Lam s (fromDeBruijn body)
@@ -53,6 +55,8 @@ toDeBruijn term = go term []
       App (go f env) (go a env)
     go (Eval.Num n) _env =
       FNum n
+    go (Eval.Str s) _env =
+      FStr s
 
 eval :: DeBruijn ann -> DeBruijn ann
 eval (App f a) =
@@ -66,6 +70,7 @@ eval' env = \case
   FV v -> case lookup v env of
     Just term -> term
     Nothing   -> FV v
+  FStr s     -> FStr s
   FBuiltin b -> FBuiltin b
   App f a ->
     let f' = eval' env f
@@ -136,6 +141,7 @@ churchFalse = Lam "f" (Lam "t" (Var "f" 1))
 -- Comparison operators return Church booleans rather than integer flags.
 tryReduce :: Text -> [DeBruijn Text] -> Maybe (DeBruijn Text)
 tryReduce name args = case (name, args) of
+  -- Integer arithmetic
   ("+",   [FNum x, FNum y]) -> Just $ FNum (x + y)
   ("-",   [FNum x, FNum y]) -> Just $ FNum (x - y)
   ("*",   [FNum x, FNum y]) -> Just $ FNum (x * y)
@@ -144,7 +150,13 @@ tryReduce name args = case (name, args) of
   ("=",   [FNum x, FNum y]) -> Just $ if x == y then churchTrue else churchFalse
   ("<",   [FNum x, FNum y]) -> Just $ if x <  y then churchTrue else churchFalse
   ("neg", [FNum x])         -> Just $ FNum (negate x)
-  _                         -> Nothing
+  -- String operations
+  ("str-concat", [FStr x, FStr y])         -> Just $ FStr (x <> y)
+  ("str-length", [FStr x])                 -> Just $ FNum (Text.length x)
+  ("str-slice",  [FNum i, FNum j, FStr x]) -> Just $ FStr (Text.take (j - i) (Text.drop i x))
+  ("str=",       [FStr x, FStr y])         -> Just $ if x == y then churchTrue else churchFalse
+  ("str<",       [FStr x, FStr y])         -> Just $ if x <  y then churchTrue else churchFalse
+  _                                        -> Nothing
 
 -- | Rebuild a left-spine application from a head and a list of arguments.
 rebuild :: DeBruijn Text -> [DeBruijn Text] -> DeBruijn Text
@@ -156,6 +168,7 @@ substitute env n arg term = case term of
     Just t  -> t
     Nothing -> FV x
   FNum _     -> term
+  FStr _     -> term
   FBuiltin _ -> term
   Var t x
     | x == n    -> arg
@@ -167,6 +180,7 @@ pretty :: DeBruijn Text -> Text
 pretty = \case
   FV x       -> x
   FNum n     -> showNum n
+  FStr s     -> "\"" <> escapeStr s <> "\""
   FBuiltin b -> b
   Var s _    -> s
   Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
@@ -175,5 +189,15 @@ pretty = \case
 -- | 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)
+  | n < 0     = "-" <> Text.pack (show (abs n))
+  | otherwise = Text.pack (show n)
+
+-- | Escape a string for pretty-printing: wrap in double-quotes and escape
+-- backslashes and double-quote characters so the output round-trips through
+-- the parser.
+escapeStr :: Text -> Text
+escapeStr = Text.concatMap escapeChar
+  where
+    escapeChar '"'  = "\\\""
+    escapeChar '\\' = "\\\\"
+    escapeChar c    = Text.singleton c
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index 324c881..104fddc 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -8,6 +8,7 @@ import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.String (IsString (..))
 import Data.Text (Text, pack)
+import qualified Data.Text as Text
 import GHC.Generics (Generic)
 
 data Term
@@ -15,6 +16,7 @@ data Term
   | Lam Text Term
   | App Term Term
   | Num Int
+  | Str Text
   deriving (Show, Read, Eq, Generic, ToJSON, FromJSON)
 
 instance IsString Term where
@@ -27,10 +29,11 @@ data Value
   = Clos EnvValue Text Term
   | VNeut Neutral
   | VNum Int
+  | VStr Text
   | Builtin Text Int [Value]
   deriving (Show, Read, Eq)
 
-data Neutral = NVar Text | NNum Int | NApp Neutral Value
+data Neutral = NVar Text | NNum Int | NStr Text | NApp Neutral Value
   deriving (Show, Read, Eq)
 
 type Env = [(Text, Term)]
@@ -43,14 +46,19 @@ newEnv = []
 -- | Arity table for every built-in operator.
 builtinArity :: Map Text Int
 builtinArity = Map.fromList
-  [ ("+",   2)
-  , ("-",   2)
-  , ("*",   2)
-  , ("div", 2)
-  , ("mod", 2)
-  , ("=",   2)
-  , ("<",   2)
-  , ("neg", 1)
+  [ ("+",          2)
+  , ("-",          2)
+  , ("*",          2)
+  , ("div",        2)
+  , ("mod",        2)
+  , ("=",          2)
+  , ("<",          2)
+  , ("neg",        1)
+  , ("str-concat", 2)
+  , ("str-length", 1)
+  , ("str-slice",  3)
+  , ("str=",       2)
+  , ("str<",       2)
   ]
 
 -- | The set of built-in names, for fast membership testing.
@@ -77,6 +85,7 @@ eval env = \case
         a' = eval env a
      in f' `seq` a' `seq` apply f' a'
   Num n -> VNum n
+  Str s -> VStr s
 
 apply :: Value -> Value -> Value
 apply f a =
@@ -86,6 +95,7 @@ apply f a =
        in eval env' body
     VNeut f' -> VNeut (NApp f' a)
     VNum n   -> VNeut (NApp (NNum n) a)
+    VStr s   -> VNeut (NApp (NStr s) a)
     -- Last argument arrives: dispatch and reduce.
     Builtin name 1 args -> dispatchBuiltin name (args ++ [a])
     -- Still waiting for more arguments: accumulate.
@@ -105,6 +115,7 @@ churchFalse = Clos builtinEnvValue "f" (Lam "t" (Var "f"))
 -- Comparison operators (= and <) return Church booleans rather than integers.
 dispatchBuiltin :: Text -> [Value] -> Value
 dispatchBuiltin name args = case (name, args) of
+  -- Integer arithmetic
   ("+",   [VNum x, VNum y]) -> VNum (x + y)
   ("-",   [VNum x, VNum y]) -> VNum (x - y)
   ("*",   [VNum x, VNum y]) -> VNum (x * y)
@@ -115,6 +126,12 @@ dispatchBuiltin name args = case (name, args) of
   ("=",   [VNum x, VNum y]) -> if x == y then churchTrue else churchFalse
   ("<",   [VNum x, VNum y]) -> if x <  y then churchTrue else churchFalse
   ("neg", [VNum x])         -> VNum (negate x)
+  -- String operations
+  ("str-concat", [VStr x, VStr y])           -> VStr (x <> y)
+  ("str-length", [VStr x])                   -> VNum (Text.length x)
+  ("str-slice",  [VNum i, VNum j, VStr x])   -> VStr (Text.take (j - i) (Text.drop i x))
+  ("str=",       [VStr x, VStr y])           -> if x == y then churchTrue else churchFalse
+  ("str<",       [VStr x, VStr y])           -> if x <  y then churchTrue else churchFalse
   -- Stuck: reconstruct a neutral application chain rooted at the builtin name.
   _ -> foldl (\acc v -> VNeut (NApp (neutralOf acc) v)) (VNeut (NVar name)) args
   where
@@ -132,8 +149,10 @@ readBack = go []
          in Lam name (go names' val')
       VNeut (NVar n)    -> Var n
       VNeut (NNum n)    -> Num n
+      VNeut (NStr s)    -> Str s
       VNeut (NApp f a)  -> App (go names (VNeut f)) (go names a)
       VNum n            -> Num n
+      VStr s            -> Str s
       -- A partial builtin reads back as a chain of applications rooted at
       -- the builtin name, e.g. Builtin "+" 1 [VNum 3]  →  App (Var "+") (Num 3)
       Builtin bname _ accumulated ->
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
index 2052398..9f0df35 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
@@ -30,9 +30,14 @@ render :: TypeError -> Text
 render (UnifyError ue) = Unify.render ue
 
 fromTerm :: Eval.Term -> ATerm ()
-fromTerm (Eval.Var x) = Var x ()
+fromTerm (Eval.Var x)     = Var x ()
 fromTerm (Eval.Lam x body) = Lam x (fromTerm body) ()
-fromTerm (Eval.App a b) = App (fromTerm a) (fromTerm b) ()
+fromTerm (Eval.App a b)   = App (fromTerm a) (fromTerm b) ()
+-- Literal values (Num, Str) are treated as typed by a fresh variable;
+-- the inferencer only needs to traverse the term structure, not inspect
+-- literal payloads.
+fromTerm (Eval.Num _)     = Var "<num>" ()
+fromTerm (Eval.Str _)     = Var "<str>" ()
 
 infer :: Eval.Term -> Either TypeError Type
 infer t = do
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
index bf92daa..b2f011b 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
@@ -14,7 +14,7 @@ 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, optional, parse, some, try)
+import Text.Megaparsec (Parsec, between, empty, errorBundlePretty, manyTill, optional, parse, some, try)
 import Text.Megaparsec.Char (alphaNumChar, char, digitChar, letterChar, space1, symbolChar)
 import qualified Text.Megaparsec.Char.Lexer as L
 
@@ -26,6 +26,7 @@ data ParseError = ParseError Text
 data AST
   = Sym Text
   | Lit Int
+  | StrLit Text
   | Abs [Text] AST
   | App AST AST [AST]
   | Def Text AST
@@ -35,6 +36,7 @@ desugar :: AST -> Term
 desugar = \case
   Sym symb -> Eval.Var symb
   Lit n -> Eval.Num n
+  StrLit s -> Eval.Str s
   Abs bound body ->
     foldr
       Eval.Lam
@@ -52,6 +54,7 @@ resugar :: Term -> AST
 resugar = \case
   Eval.Var s -> Sym s
   Eval.Num n -> Lit n
+  Eval.Str s -> StrLit s
   Eval.Lam x body -> case resugar body of
     Abs vars ast -> Abs (x : vars) ast
     other -> Abs [x] other
@@ -67,10 +70,21 @@ pretty :: AST -> Text
 pretty = \case
   Sym symb -> symb
   Lit n -> prettyInt n
+  StrLit s -> "\"" <> escapeString s <> "\""
   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 <> ")"
 
+-- | Escape special characters in a string literal for pretty-printing.
+-- Only @\"@ and @\\@ need escaping; the parser uses 'L.charLiteral' which
+-- understands standard Haskell escape sequences.
+escapeString :: Text -> Text
+escapeString = Text.concatMap go
+  where
+    go '"'  = "\\\""
+    go '\\' = "\\\\"
+    go c    = Text.singleton c
+
 -- | Render an integer with no space between '-' and digits for negative numbers.
 prettyInt :: Int -> Text
 prettyInt n
@@ -87,7 +101,7 @@ parse =
   first (ParseError . pack . errorBundlePretty) . Text.Megaparsec.parse ast ""
 
 ast :: Parser AST
-ast = try defExpr <|> try letExpr <|> try lambda <|> try lit <|> try sym <|> try app
+ast = try defExpr <|> try letExpr <|> try lambda <|> try strLit <|> try lit <|> try sym <|> try app
 
 app :: Parser AST
 app =
@@ -163,6 +177,14 @@ lit = lexeme $ do
     Just _  -> negate n
     Nothing -> n
 
+-- | Parse a double-quoted string literal.
+-- Uses 'L.charLiteral' for each character so that standard Haskell escape
+-- sequences (e.g. @\"@, @\\@, @\n@, @\t@) are handled automatically.
+strLit :: Parser AST
+strLit = lexeme $ do
+  chars <- char '"' *> manyTill L.charLiteral (char '"')
+  pure $ StrLit $ pack chars
+
 sym :: Parser AST
 sym = Sym . pack <$> identifier
 
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
index eaff77c..f1802da 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
@@ -81,3 +81,37 @@ spec = do
 
     it "lookup of '+' in builtin env yields FBuiltin" $
       eval' benv (FV "+") `shouldBe` FBuiltin "+"
+
+  describe "string literals and builtins" $ do
+    let benv = builtinDeBruijnEnv :: Env Text
+
+    it "FStr self-evaluates" $
+      eval' benv (FStr "hello") `shouldBe` FStr "hello"
+
+    it "(str-concat \"foo\" \"bar\") reduces to FStr \"foobar\"" $
+      eval' benv (App (App (FBuiltin "str-concat") (FStr "foo")) (FStr "bar"))
+        `shouldBe` FStr "foobar"
+
+    it "(str-length \"hello\") reduces to FNum 5" $
+      eval' benv (App (FBuiltin "str-length") (FStr "hello"))
+        `shouldBe` FNum 5
+
+    it "(str-slice 1 3 \"abcde\") reduces to FStr \"bc\"" $
+      eval' benv (App (App (App (FBuiltin "str-slice") (FNum 1)) (FNum 3)) (FStr "abcde"))
+        `shouldBe` FStr "bc"
+
+    it "(str= \"abc\" \"abc\") reduces to Church True" $
+      eval' benv (App (App (FBuiltin "str=") (FStr "abc")) (FStr "abc"))
+        `shouldBe` Lam "f" (Lam "t" (Var "t" 0))
+
+    it "(str= \"abc\" \"xyz\") reduces to Church False" $
+      eval' benv (App (App (FBuiltin "str=") (FStr "abc")) (FStr "xyz"))
+        `shouldBe` Lam "f" (Lam "t" (Var "f" 1))
+
+    it "(str< \"a\" \"b\") reduces to Church True" $
+      eval' benv (App (App (FBuiltin "str<") (FStr "a")) (FStr "b"))
+        `shouldBe` Lam "f" (Lam "t" (Var "t" 0))
+
+    it "(str-concat \"hello\") is partial: stays as App spine" $
+      eval' benv (App (FBuiltin "str-concat") (FStr "hello"))
+        `shouldBe` App (FBuiltin "str-concat") (FStr "hello")
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index e5075f0..96fff08 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -11,6 +11,7 @@ import Minilang.Lambda (loadProgram)
 import qualified Minilang.Lambda.DeBruijn as DB
 import Minilang.Lambda.DeBruijn (toDeBruijn)
 import Minilang.Lambda.Eval (Env, Term (..), Value (..), eval, normalise, builtinEnvValue, newEnv)
+import qualified Data.Text as Text
 import Minilang.Lambda.Infer (newContext)
 import Minilang.Lambda.Parser (parseProgram)
 import Minilang.REPL.Types (Evaluator (..), Language (..))
@@ -196,6 +197,101 @@ spec = do
       normalise (App (App (Var "mod") (Num 5)) (Num 0))
         `shouldBe` App (App (Var "mod") (Num 5)) (Num 0)
 
+  describe "string literals and builtins" $ do
+    -- Self-evaluation
+    it "string literal evaluates to itself" $
+      normalise (Str "hello") `shouldBe` Str "hello"
+
+    it "empty string evaluates to itself" $
+      normalise (Str "") `shouldBe` Str ""
+
+    prop "any string literal normalises to itself" $ \s ->
+      normalise (Str (Text.pack s)) === Str (Text.pack s)
+
+    -- eval produces VStr
+    prop "eval of a string literal produces VStr" $ \s ->
+      eval [] (Str (Text.pack s)) === VStr (Text.pack s)
+
+    -- String in function position is stuck
+    it "string in function position produces a stuck application" $
+      normalise (App (Str "oops") (Var "x"))
+        `shouldBe` App (Str "oops") (Var "x")
+
+    -- str-concat
+    it "(str-concat \"foo\" \"bar\") == \"foobar\"" $
+      normalise (App (App (Var "str-concat") (Str "foo")) (Str "bar"))
+        `shouldBe` Str "foobar"
+
+    it "(str-concat \"\" \"abc\") == \"abc\"" $
+      normalise (App (App (Var "str-concat") (Str "")) (Str "abc"))
+        `shouldBe` Str "abc"
+
+    prop "str-concat is associative" $ \a b c ->
+      let s x = Str (Text.pack x)
+          cat x y = App (App (Var "str-concat") x) y
+      in normalise (cat (cat (s a) (s b)) (s c))
+           === normalise (cat (s a) (cat (s b) (s c)))
+
+    -- str-length
+    it "(str-length \"hello\") == 5" $
+      normalise (App (Var "str-length") (Str "hello")) `shouldBe` Num 5
+
+    it "(str-length \"\") == 0" $
+      normalise (App (Var "str-length") (Str "")) `shouldBe` Num 0
+
+    prop "str-length of concat equals sum of lengths" $ \a b ->
+      let sa = Text.pack a; sb = Text.pack b
+      in normalise (App (Var "str-length") (App (App (Var "str-concat") (Str sa)) (Str sb)))
+           === normalise (App (App (Var "+") (App (Var "str-length") (Str sa)))
+                                             (App (Var "str-length") (Str sb)))
+
+    -- str-slice
+    it "(str-slice 1 3 \"abcde\") == \"bc\"" $
+      normalise (App (App (App (Var "str-slice") (Num 1)) (Num 3)) (Str "abcde"))
+        `shouldBe` Str "bc"
+
+    it "(str-slice 0 0 \"abc\") == \"\"" $
+      normalise (App (App (App (Var "str-slice") (Num 0)) (Num 0)) (Str "abc"))
+        `shouldBe` Str ""
+
+    -- str= (Church booleans)
+    it "(str= \"abc\" \"abc\") == Church True" $
+      normalise (App (App (Var "str=") (Str "abc")) (Str "abc"))
+        `shouldBe` Lam "f" (Lam "t" (Var "t"))
+
+    it "(str= \"abc\" \"xyz\") == Church False" $
+      normalise (App (App (Var "str=") (Str "abc")) (Str "xyz"))
+        `shouldBe` Lam "f" (Lam "t" (Var "f"))
+
+    prop "str= is reflexive" $ \s ->
+      normalise (App (App (Var "str=") (Str (Text.pack s))) (Str (Text.pack s)))
+        === Lam "f" (Lam "t" (Var "t"))
+
+    -- str<
+    it "(str< \"abc\" \"abd\") == Church True" $
+      normalise (App (App (Var "str<") (Str "abc")) (Str "abd"))
+        `shouldBe` Lam "f" (Lam "t" (Var "t"))
+
+    it "(str< \"b\" \"a\") == Church False" $
+      normalise (App (App (Var "str<") (Str "b")) (Str "a"))
+        `shouldBe` Lam "f" (Lam "t" (Var "f"))
+
+    -- Partial application
+    it "(str-concat \"hello\") is partial" $
+      eval builtinEnvValue (App (Var "str-concat") (Str "hello"))
+        `shouldBe` Builtin "str-concat" 1 [VStr "hello"]
+
+    -- Stuck: free variable argument
+    it "(str-concat x \"bar\") with free x stays stuck" $
+      normalise (App (App (Var "str-concat") (Var "x")) (Str "bar"))
+        `shouldBe` App (App (Var "str-concat") (Var "x")) (Str "bar")
+
+    -- Higher-order: pass builtin as function
+    it "str-concat passed as higher-order argument works" $
+      normalise (App (Lam "f" (App (App (Var "f") (Str "hello")) (Str " world")))
+                     (Var "str-concat"))
+        `shouldBe` Str "hello world"
+
   describe "evaluator equivalence on challenges" $ do
     challenges <- runIO $
       eitherDecodeFileStrict "challenges.json" >>= \case
@@ -243,6 +339,7 @@ challengeEquivalenceTest env Challenge{level, expr} =
 eraseNames :: DB.DeBruijn Text -> DB.DeBruijn ()
 eraseNames (DB.FV x)       = DB.FV x
 eraseNames (DB.FNum n)     = DB.FNum n
+eraseNames (DB.FStr s)     = DB.FStr s
 eraseNames (DB.FBuiltin b) = DB.FBuiltin b
 eraseNames (DB.Var _ i)    = DB.Var () i
 eraseNames (DB.Lam _ body) = DB.Lam () (eraseNames body)
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
index 08ec661..40866bb 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
@@ -10,7 +10,7 @@ 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 Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars, escapeString)
 import Minilang.Lambda.Eval (normalise)
 import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy)
 import Test.Hspec.QuickCheck (prop)
@@ -175,6 +175,115 @@ spec = parallel $ do
     it "pretty (+ 1) is \"(+ 1)\"" $
       pretty (App (Sym "+") (Lit 1) []) `shouldBe` "(+ 1)"
 
+  describe "string literals" $ do
+    -- Round-trip: parse . pretty == id for all safe StrLit values
+    prop "any StrLit rendered by pretty parses back to the same StrLit" $
+      forAll genStrLit $ \ast ->
+        parse (pretty ast) === Right ast
+
+    it "parses empty string literal" $
+      parse "\"\"" `shouldBe` Right (StrLit "")
+
+    it "parses simple string literal" $
+      parse "\"hello\"" `shouldBe` Right (StrLit "hello")
+
+    it "parses string with spaces" $
+      parse "\"foo bar\"" `shouldBe` Right (StrLit "foo bar")
+
+    it "parses escaped double-quote inside string" $
+      parse "\"say \\\"hi\\\"\"" `shouldBe` Right (StrLit "say \"hi\"")
+
+    it "parses escaped backslash inside string" $
+      parse "\"back\\\\slash\"" `shouldBe` Right (StrLit "back\\slash")
+
+    it "pretty-prints string with double-quote escaped" $
+      pretty (StrLit "say \"hi\"") `shouldBe` "\"say \\\"hi\\\"\""
+
+    it "pretty-prints string with backslash escaped" $
+      pretty (StrLit "back\\slash") `shouldBe` "\"back\\\\slash\""
+
+    -- desugar / normalise
+    it "desugar and normalise string self-evaluates" $
+      normalise (desugar (StrLit "hello")) `shouldBe` Eval.Str "hello"
+
+    it "desugar and normalise str-concat" $
+      normalise (desugar (App (Sym "str-concat") (StrLit "foo") [StrLit "bar"]))
+        `shouldBe` Eval.Str "foobar"
+
+    it "desugar and normalise str-length" $
+      normalise (desugar (App (Sym "str-length") (StrLit "hello") []))
+        `shouldBe` Eval.Num 5
+
+    it "desugar and normalise str-slice" $
+      normalise (desugar (App (Sym "str-slice") (Lit 1) [Lit 3, StrLit "abcde"]))
+        `shouldBe` Eval.Str "bc"
+
+    it "desugar and normalise str= equal strings gives Church True" $
+      normalise (desugar (App (Sym "str=") (StrLit "abc") [StrLit "abc"]))
+        `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "t"))
+
+    it "desugar and normalise str= unequal strings gives Church False" $
+      normalise (desugar (App (Sym "str=") (StrLit "abc") [StrLit "xyz"]))
+        `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "f"))
+
+    it "partial str-concat pretty-prints as application" $
+      pretty (App (Sym "str-concat") (StrLit "hello") [])
+        `shouldBe` "(str-concat \"hello\")"
+
+  describe "strings containing parentheses" $ do
+    -- The parser must not treat ( or ) inside a string literal as
+    -- delimiters for an application or lambda expression.
+
+    it "parses a string containing only an opening paren" $
+      parse "\"(\"" `shouldBe` Right (StrLit "(")
+
+    it "parses a string containing only a closing paren" $
+      parse "\")\"" `shouldBe` Right (StrLit ")")
+
+    it "parses a string containing balanced parens" $
+      parse "\"(hello)\"" `shouldBe` Right (StrLit "(hello)")
+
+    it "parses a string containing doubly-nested parens" $
+      parse "\"((nested))\"" `shouldBe` Right (StrLit "((nested))")
+
+    it "parses a string containing unbalanced parens" $
+      parse "\"a(b\"" `shouldBe` Right (StrLit "a(b")
+
+    it "parses a string that looks like a lambda expression" $
+      parse "\"(lam (x) x)\"" `shouldBe` Right (StrLit "(lam (x) x)")
+
+    it "parses a string that looks like an application" $
+      parse "\"(f x)\"" `shouldBe` Right (StrLit "(f x)")
+
+    -- Round-trip: pretty-printing a StrLit with parens re-parses correctly
+    it "pretty-prints and re-parses string with opening paren" $
+      parse (pretty (StrLit "(")) `shouldBe` Right (StrLit "(")
+
+    it "pretty-prints and re-parses string with balanced parens" $
+      parse (pretty (StrLit "(hello)")) `shouldBe` Right (StrLit "(hello)")
+
+    it "pretty-prints and re-parses string with doubly-nested parens" $
+      parse (pretty (StrLit "((x))")) `shouldBe` Right (StrLit "((x))")
+
+    -- Property: any string containing only parens and letters round-trips
+    prop "strings with parentheses round-trip through pretty and parse" $
+      forAll (StrLit . Text.pack <$> listOf (elements "abcdef()")) $ \ast ->
+        parse (pretty ast) === Right ast
+
+    -- The paren-containing string is correctly passed through an application
+    it "paren string survives beta-reduction" $
+      normalise (desugar (App (Abs ["x"] (Sym "x")) (StrLit "(hello)") []))
+        `shouldBe` Eval.Str "(hello)"
+
+    -- str-concat of two paren strings
+    it "str-concat of paren strings produces correct result" $
+      normalise (desugar (App (Sym "str-concat") (StrLit "(") [StrLit ")"]))
+        `shouldBe` Eval.Str "()"
+
+    it "str-length of paren string counts parens" $
+      normalise (desugar (App (Sym "str-length") (StrLit "(hello)") []))
+        `shouldBe` Eval.Num 7
+
   it "parses multiline program with blank lines" $ do
     let program =
           "(def id (lam (x) x))\n\
@@ -230,6 +339,7 @@ instance Arbitrary AST where
   shrink = \case
     Sym _ -> []
     Lit _ -> []
+    StrLit _ -> []
     Abs bind body -> case shrink (Identifier <$> bind) of
       [] -> shrink body
       bind' ->
@@ -245,15 +355,24 @@ instance Arbitrary AST where
     Def _name body -> shrink body -- never generated
 
 genAst :: Int -> Gen AST
-genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary]
+genAst 0 = oneof [Sym . unIdent <$> arbitrary, Lit <$> arbitrary, genStrLit]
 genAst depth =
   oneof
     [ Sym . unIdent <$> arbitrary
     , Lit <$> arbitrary
+    , genStrLit
     , genAbstraction depth
     , genApplication depth
     ]
 
+-- | Generate a random string literal. We restrict the alphabet to printable
+-- ASCII excluding @\"@ and @\\@ to keep round-trip tests simple; the escape
+-- logic is tested separately.
+genStrLit :: Gen AST
+genStrLit = StrLit . pack <$> listOf (elements safeChars)
+  where
+    safeChars = filter (\c -> c /= '"' && c /= '\\') [' '..'~']
+
 genDef :: Int -> Gen AST
 genDef n = Def . unIdent <$> arbitrary <*> genAst n