When University of Copenhagen lecturer Torben Ægidius Mogensen posed exam questions about termination properties in a minimal functional language, student Mark Seemann did more than theorize—he built a working interpreter. The resulting implementation, shared in a technical deep dive, offers masterclass insights into language design fundamentals.

The Bopa Language: Booleans, Pairs, and Constraints

The language—dubbed "Bopa" for its Boolean/Pair foundation—features intentionally restricted semantics:

-- Core AST Types

type Program = NonEmpty Function
data Pattern = VarPat String | TPat | FPat | PairPat Pattern Pattern
data Exp = VarExp String | TExp | FExp | CallExp String (NonEmpty Exp)

Key constraints include:
- No partial application (all functions fully applied)
- Disjoint pattern matching rules
- Values limited to booleans and pairs
- No higher-order functions

These limitations make termination analysis tractable—a core focus of the original exam.

Parsec-Powered Parsing: From Text to AST

Seemann implemented the frontend using Haskell's parsec combinator library. The parser elegantly handles the grammar's nuances:

functionParser :: Stream s m Char => ParsecT s () m Function
functionParser = do
  fnid <- many1 lower
  let pp = many1 (char ' ') >> patternParser
  patterns <- (:|) <$> pp <*> pp `manyTill` try (many1 (char ' ') >> char '=')
  skipMany1 (char ' ')
  Function fnid patterns <$> expParser

The implementation demonstrates pragmatic tradeoffs: minimal error handling, no test suite, and deliberate code duplication in exchange for rapid iteration—hallmarks of exploratory coding.

The Interpreter's Secret Weapon: Pattern Matching Semantics

The evaluation engine hinges on two critical functions:

  1. tryBind: Matches patterns to arguments, building variable environments
  2. tryMatch: Selects the first matching function rule
-- Simplified matching logic
tryBind (VarPat p :| []) (arg :| []) = Right [(p, arg)]
tryBind (PairPat p1 p2 :| []) (PairArg a1 a2 :| []) = 
  (++) <$> tryBind [p1] [a1] <*> tryBind [p2] [a2]

Crucially, the interpreter includes cycle detection to enforce termination:

eval observedCalls prog env (CallExp fnid exps) = do
  -- ...
  if Set.member (fnid, args) observedCalls 
  then Left "Cycle detected."
  else eval (Set.insert (fnid, args) observedCalls) prog env' body

Why This Matters Beyond the Exam

  1. Educational Blueprint: The 300-line implementation demonstrates compiler fundamentals in digestible form
  2. Termination Proof: By design, Bopa programs always terminate (verified via cycle checks)
  3. Real-World Parallels: The pattern-matching approach mirrors real functional languages like Haskell and ML

Seemann reflects: "Implementing the interpreter helped me articulate why termination is decidable for this language—sometimes code speaks louder than proofs." The exercise underscores how constrained languages enable formal guarantees impossible in Turing-complete systems.

Experimentation remains open: Try the complete implementation or extend it with recursion or basic arithmetic. Just don't expect Turing completeness—that's precisely the point.