Discover how a programming languages exam question about termination properties inspired a full Haskell implementation of a tiny functional language interpreter. This deep dive explores parser combinator design, pattern matching mechanics, and why this deliberately limited language isn't Turing complete.
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:
tryBind: Matches patterns to arguments, building variable environmentstryMatch: 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
- Educational Blueprint: The 300-line implementation demonstrates compiler fundamentals in digestible form
- Termination Proof: By design, Bopa programs always terminate (verified via cycle checks)
- 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.

Comments
Please log in or register to join the discussion