SECD

A Haskell implementation of the SECD abstract machine, a classic virtual machine for evaluating lambda calculus expressions. It includes a small Lisp-like frontend language (MicroLisp) that compiles to SECD instructions.

Overview

The SECD machine operates on four registers:

• Stack -- operand stack for intermediate results
• Environment -- variable bindings (using de Bruijn indices)
• Control -- instruction sequence to execute
• Dump -- saved state for function returns

Instruction Set

Instruction	Description
IInt n	Push integer n onto the stack
IAdd	Pop two integers and push their sum
ISub	Pop two integers and push their difference
IAccess n	Push the n-th value from the environment
IClosure c	Create a closure with code c and the current environment
IApply	Apply a closure to an argument
IReturn	Restore state from the dump

Compilation Pipeline

MicroLisp source code is compiled through the following stages:

Source String -> S-Expression -> Lambda Term -> De Bruijn Term -> SECD Instructions

1. Parsing -- S-expression parser (parsec)
2. Term construction -- Convert S-expressions into lambda terms with named variables
3. De Bruijn indexing -- Replace named variables with positional indices
4. Code generation -- Emit SECD instruction sequences

MicroLisp

MicroLisp is a minimal Lisp dialect that serves as the frontend language. It supports:

• Integers -- 0, 1, 42
• Arithmetic -- (+ 1 2), (- 10 3)
• Lambda -- (lambda (x) body) (single parameter)
• Function application -- (f arg)
• Comments -- # this is a comment

Nested expressions and higher-order functions work as expected:

# apply a function to double its argument
((lambda (x) (+ x x)) 5)    # => 10

# function composition
((lambda (f)
  ((lambda (g)
    (f (g 1)))
  (lambda (x) (+ x x))))
(lambda (x) (+ x 1)))       # => 3

Variables are lexically scoped. The compiler converts named variables to de Bruijn indices before generating SECD instructions.

Usage

Build and run the interactive REPL:

$ stack build
$ stack exec secdi

Run a program from a file:

$ stack exec secdi -- examples/church.ml
10

REPL Examples

% (+ 1 2)
3
% ((lambda (x) (+ x x)) 2)
4
% ((lambda (x) (+ x 1)) 10)
11
% quit

Project Structure

src/
  SECD/
    Types.hs          -- MValue, Command, SECD type definitions
    Eval.hs           -- SECD machine step function and evaluator
  SECD.hs             -- Re-exports SECD modules
  Language/
    MicroLisp/
      SExprParser.hs  -- S-expression parser
      Compiler.hs     -- Compilation pipeline (parsing, de Bruijn, codegen)
    MicroLisp.hs      -- Re-exports MicroLisp modules
secdi/
  Main.hs             -- Interactive REPL using haskeline

Building

Requires Stack or GHCup.

$ stack build
$ stack test

License

BSD-3-Clause