First Draft: Little Haskell Compiler Adventures: The SECD Machine

Show and Tell
1

STATUS: This article is a little bit rough, but I’ve been working on it long enough that its worth publishing now, and editing to fix anything. I really should have published it earlier, because I actually broke the character limit on posts and had to split it up - that’s a first. I tried to write a shorter article, and it ended up being my longest ever.

Consider it to be a first draft of what will be more properly edited and published in the future as part of a series.

NOTE: The source repository is not up yet, it will be available soon.

A joke to set the tone

A SECD machine tries to walk into a Haskell bar, but gets stopped by the bouncer.

“Hey, I have to see your \ x -> x before you can come inside.”

“Oh, sure. Here it is.” The SECD machine hands the bouncer an [ LD, Index 0 0, RTN ] and the bouncer looks at them through it. The bouncer stares at the odd-looking code, which doesn’t do seem to do anything, nor should it.

“Its valid Haskell syntax, I promise.” The bouncer looks closer, and sure enough, it is. And when he looks through it at the strange machine standing before him, nothing has changed.

“It’s a little hard to parse, but I guess it checks out”

“Yes, I still have a bit of a Lisp, but I’m working on it - I hope that’s okay.”

“Yeah, so long as you’re functional. Alright, you can go on in.”

“Thanks.”

The bouncer opens the door to the bar, and the SECD machine walks inside.

Advantages of the SECD machine

I’ve always been a fan of Ben Lynn’s Compiler Quest series on building a self-hosted compiler with minimal fuss, and I’ve always wanted to emulate its practical approach that gets straight to the point. So, I’m building a self-hosted Haskell compiler based on the SECD machine. I call it the Little Haskell Compiler, or LHC for short.

The SECD machine is a tiny, easy-to-understand virtual machine invented by Peter Landin way back in 1971 as the first ever machine designed to evaluate lambda calculus. More than a historical curiosity, it presents many advantages:

  • It is easy to understand and implement.

A working implementation of a SECD machine can be written C or Haskell in just a couple hundred lines of code.

  • It is easy to hand-debug

It has only 4 registers, and 24-ish opcodes, most of which are short sequences of stack pushes and pops.

  • It is homoiconic

The register / control stacks are themselves cons-cells, and you can print the registers and machine memory to trace what has happened. Its how Pure Lisp was implemented.

  • It is relocatable and portable

A SECD program can easily be paused, moved to another region of memory or even another computer, and resumed there for execution.

  • It is write-once, read-only

A SECD machine is a tape machine with linear access to read-only memory. This has practical implications for distributed and append-only data structures.

  • It can easily be extended with new functionality

It is easy to optimize a SECD machine with custom opcodes or by giving it a traditional heap for random-access memory and data structures

  • It is easy to integrate foreign function calls

A SECD VM can share atom data types with the host language, making it a free implementation of closures for languages like C. If it is running on bare metal, it uses the architecture word type as its atom type.

  • It is excellent for scripting

I can write a hello world program that fits in a few hundred cells, making it possible to pass around tiny programs.

These are the reasons I have chosen it as the base machine of my compiler. This also makes it fairly unique among Haskell variants:

  • GHC is a STG machine
  • MicroHS is a combinator machine
  • Hugs is a bytecode interpreter

Now, the LHC is a SECD machine.

Disadvantages of the SECD machine

The SECD machine comes with a few challenges. A naive implementation will face:

  • Slow environment variable lookup
  • High memory overhead
  • Memory fragmentation and cache misses
  • Low code density and inflated binary size

Most of these can be mitigated with additional opcodes for efficiency, or by adding a traditional heap, and by flattening some of the linked lists data structures into arrays and structs - and we all know linked lists have their advantages too since Haskell uses linked lists as a control structure quite heavily.

Another challenge, is the relative obscurity of the SECD machine itself. Almost all the materials I found while researching it fell into one or more of the following categories:

  • Non-OCR PDF scans of literal paper documents
  • Were written in Lisp
  • Made heavy usage of non-canonical opcodes
  • Weren’t even SECD machines because they didn’t even have the right registers
  • Used host pointers instead of cell addresses
  • Used malloc and free everywhere all the time
  • Implemented basic things wrong

Of all of these, the most helpful resources were:

These are the only materials that actually correlated with each other, so I assumed that they were the best resources, and I’d just have to deal with translating Lisp for a bit, and de-snarling the Lispkit’s direct pointer usage in favor of relocatable addresses.

Even the secd package in Haskell isn’t a full SECD machine - it only has three registers and four opcodes not counting the int atom and arithmetic functions, and it relies almost entirely on the Haskell runtime to perform the missing functions such as managing the dump or handling recursion. I can’t translate that to C, I’d need to have a full Haskell runtime to do that, which is what I’m writing in the first place.

What is a SECD machine?

This is mostly a deep dive into a Haskell translation of the Lisp blog. I envy its compactness and succinctness, and if you can read Lisp, its worth consulting to follow along.

The SECD machine is a 4-register stack machine that uses cons-cells in the same way that Haskell uses lists. In a SECD machine, everything is a cons-cell.

So, what is a cons-cell?

Cons Cells

A cons cell is either nil, or a pair of cons cells, plus any sort of ancillary data.

data Cell
    = Nil
    | Cons Cell Cell
    | ... ATOMS AND OPCODES LATER

You may notice that it is isomorphic to Fix List aka a list that contains more lists as values, so we could define it this way, using actual Haskell lists.

data List a
    = Nil
    | Cons a (List a)

data Fix f = Fix (f (Fix f))

type Cell = Fix List

This means that it can play the part of a pair OR a list, because it is both. Remember, a pair is isomorphic to a nil-terminated list of two values. You can turn Cons x last into Cons x (Cons last Nil) and vice versa by stripping or adding the implied last two Cons and Nil, depending on whether you want to either save space, or have simpler push and pop operations.

In my machine, I am currently reserving pairs for closures and indices, and require that all my cons-lists be properly encoded as nil-terminated lists for better compatibility with Haskell syntax and to simplify push / pop operations in the C VM. I think this is a minor deviation that is worthwhile and has no effect on the machine otherwise.

It turns out you can encode anything using cons-cells, just like you can encode anything using lambda calculus. This is why I am using cons-cells. It is easy to encode a peano number using a cons-list:

three = Cons Nil (Cons Nil (Cons Nil Nil)) -- Equivalent to [[],[],[]]

Atoms

Encoding integers using peano numbers is inefficient, and I want to be able to interact with the host environment, so I have added Int as an Atom type for our cons-cell. An atom is just a value that fits in a single cell.

Theoretically, if we had a lot of atom types, I could make a separate Atom data type, like so:

data Atom
    = Unit
    | Bool   Bool
    | Int8   Int8
    | Int16  Int16
    | Int32  Int32
    | Int64  Int64
    | Word8  Word8
    | Word6  Word6
    | Word32 Word32
    | Word64 Word64
    | Heap   (Ptr Word8)
    | Char   Char
    | String String
    | Bytes  ByteString
    | Fn     (Atom -> Atom)

data Cell
    = Nil
    | Cons Cell Cell
    ...
    | Atom Atom

Implementing that many atoms would get in the way of demonstrating the SECD machine, so instead I’ve chosen to inline the single Int atom constructor into the Cell data type for simplicity:

data Cell
    = Nil
    | Cons Cell Cell
    | Atom Int

With atoms, we can start defining meaningful values:

five :: Cell
five = Atom 5

nums :: Cell
nums = Cons (Atom 1) (Cons (Atom 2) (Cons (Atom 3) Nil))

That’s ugly. I’ll give Cell a few incomplete instances to make it easier to work with:

instance IsList Cell where
    type Item Cell = Cell
    fromList [] = Nil
    fromList [x] = Cons x Nil
    fromList (x:xs) = Cons x (fromList xs)

instance Num Cell where
    fromInteger n = Atom (fromInteger n)

Don’t do this.

Having to fall back on incomplete instances like this are why I want to extract integer literals from the Num class, which I’m going to do in my compiler. Consider the LHC to be a testbed for several of my unofficial proposals.

Normally this is extremely bad, but this is an educational article, and it helps me declare data a lot more clearly:

five :: Cell
five = 5

nums :: Cell
nums = [ 1, 2, 3 ]

This allows me to begin making Haskell homoiconic, by making Haskell list and literal syntax actually generate cons-cells. Unfortunately, OverloadedLists and IsList do not seem to allow me to overload : to mean Cons - another potential future proposal for the LHC to test.

This is one of several examples of hardcoded or typeclass-defined operators in base that get in the way of Haskell becoming homoiconic, and so this is another way LHC Haskell will deviate from GHC Haskell. In the LHC, : will actually mean Cons as in Cons cells, and the exposed List type will be backed by it. This generalizes Haskell list syntax to cons cells. Until then, we’re stuck with pattern matching a lot of Cons x y instead of x:y.

If I took . away from compose, I could make [ x . y ] mean the same thing as (x,y) giving us the ability to use the pair-terminated list syntax like lisp. I’m not entirely sure I want to, but I’m also kind of curious, because it furthers the homoiconicism which means it is possibly worth losing dot-compose, especially since we have <<< which matches <=< so maybe its not fatal.

Continuing the direction towards homoiconicism, I have also given it an instance (not shown) of Show to pretty print cons lists using Haskell List syntax:

instance Show Cell where
    showsPrec Nil = "[]"
    showsPrec (Cons car cd) = ...

putStrLn $ show $ [ LDC, 1, LDC, 2, ADD, STOP ]
-- "[ LDC, 1, LDC, 2, ADD, STOP ]'

The opcodes

In addition to atom values, cons cells can also hold opcode instructions. I’ll list them all here briefly, and I’ll explain each of them individually later, one by one.

Each opcode falls into a category:

data Opcode
    = ABRT -- Non-canonical panic
    -- Constructing cons cells
    | NIL
    | NULL
    | CONS
    | CAR
    | CDR
    -- Loading constants and variables
    | LDC
    | LD
    -- Loading and applying functions
    | LDF
    | AP
    | RTN
    -- Branching
    | SEL
    | JOIN
    -- Recursive contexts
    | DUM
    | RAP
    -- Atom functions
    | ATOM
    | EQ
    | LEQ
    | ADD
    | SUB
    | MUL
    | DIV
    | REM
    -- Stop the program
    | STOP
    -- ... OPCODE EXTENSIONS

Only 14 opcodes, NIL through RAP, are actually required - the other 10 are optional. DUM and RAP are optional, too, if you do not have recursive code or the host environment handles it. NIL is also optional, if defined as LDC Nil. I believe that CAR and CDR can also be defined using LDF, leaving you with just 11 opcodes, but it is significantly inefficient to do so.

I could integrate the opcodes into our cell like so:

data Cell
    = Nil
    | Cons Cell Cell
    | Atom Int
    | Opcode Opcode

And this is how I want you to think of it, but, like with the atoms, I will actually need to inline these opcode constructors into the Cell data type. Otherwise, I would have to preface each opcode with “Opcode”, breaking the homoiconicism.

So it actually looks like this:

data Cell
    = Nil
    | Cons Cell Cell
    | Atom Int
    | ABRT
    | NIL
    | NULL
    | CONS
    | CAR
    | CDR
    | LDC
    | LD
    | LDF
    | AP
    | RTN
    | SEL
    | JOIN
    | DUM
    | RAP
    | ATOM
    | EQ
    | LEQ
    | ADD
    | SUB
    | MUL
    | DIV
    | REM
    | STOP

That’s it! That’s all you need to write control sequences like [ LDC, 1, LDC, 2, ADD ] or full programs with nested code branches [ NIL, NULL, SEL, [LDC, 99, JOIN], [LDC, 100, JOIN], STOP ] - that’s a full program defined in syntax that is both valid SECD and Haskell.

But how are these programs run?

Continued in the next post due to breaking the character limit

4 Likes
2

The machine

The SECD machine is a 4-register stack machine that uses cons-cells in the same way that Haskell uses lists. The four registers are the stack, env, control, and dump, hence the name, SECD.

In a SECD machine, everything is a cons-cell, even the four registers.

-- The registers
type Stack   = Cell -- Conceptually, [Cell], but Cell is already a list
type Env     = Cell
type Control = Cell
type Dump    = Cell

-- The machine itself
type Machine = (Stack, Env, Control, Dump)

More specifically, each of the registers is a cons-list, and since we can list syntax for cons-lists, we can initialize our machine with a bunch of empty lists:

emptyMachine = ([], [], [], [])

By default, the empty machine represents a failure state, much like an empty parser. Instead, we should initialize it with some code. Since initializing a quadruple tuple is inconvenient, I define a convenience function for loading programs:

load prog = ([], [], prog, [])

Now, I can easily define and load programs:

machine = load [ LDC, 1, LDC, 2, ADD, STOP ]

Even though I haven’t bothered defining what the opcodes do, it is clear this program adds two numbers, (and less clearly, ends with the result on the stack).

But how does this run?

The state transitions

In a SECD machine, each opcode performs a state transition (s, e, c, d) -> (s', e', c', d') when it is popped from the control stack. Each state transition may push or pop multiple values to and from any of the registers, including the register stacks themselves. For each opcode, I will illustrate the transition in a comment in a simple format that uses : as `Cons’ and drops the quadruple parenthesis and commas.

I have also added a status code to tell when the machine has halted instead of relying on detecting an empty control stack.

data Status = Ready | Stopped | Aborted

step :: Machine -> (Machine, Status)
step = ...

Halting conditions: STOP and ABRT

The machine perform transitions until it is told to STOP with a result, it encounters an ABRT condition, or it has exhausted a malformed control stack:

-- s e [] d -> Aborted.
-- s e (ABRT:c) d -> Aborted.
-- s e (STOP:c) d -> Stopped with optional result on the stack. 
step (s, e, [], d) = ((s, e, [], d), Aborted)
step (s, e, (Cons ABRT c), d) = ((s, e, c, d), Aborted)
step (s, e, (Cons STOP c), d) = ((s, e, c, d), Stopped)
...

All other opcodes should return the status Ready unless they encounter a malformed structure.

NIL and NULL

The NIL opcode pushes a Nil value onto the stack:

-- s e (NIL:c) d -> ([]:s) e c d
step (s, e, Cons NIL c, d) = ((Cons [] s, e c, d), Ready)
...

The NULL opcode pops a value from the stack, checks whether or not it is Nil,
and then pushes a truth value 0 or 1 onto the stack.

null :: Cell -> Cell
null x = if x == [] then 1 else 0
-- Or, using pattern matching to avoid needing eq
null [] = 1
null _  = 0

-- (x:s) e (NULL:c) d -> ((null x):s) e c d
step (Cons x s, e, Cons NULL c, d) = ((Cons (null x) s, e c, d), Ready)
...

Therefore, loading the following instruction sequence: [ NIL, NULL, STOP ] should result in the following machine actions and states:

  • The initial state ([], [], [ NIL, NULL, STOP ], [])
  • Push a Nil onto the stack
  • ([[]], [], [ NULL, STOP ], [])
  • Pop the stack
  • Check if the value is null / a Nil
  • Push the resulting true value (1 in this case) onto the stack
  • ([1], [], [ STOP ], [])
  • Stop the machine with the final state ([1], [], [], [])

Yes, indeed null [].

I know that NIL Nil and NULL can be confusing, so just remember that ALLCAPS are opcodes. NIL makes a Nil, and NULL checks if a thing is Nil, and both NIL nor NULL have opcode values, meaning they aren’t themselves Nil.

CONS CAR and CDR

So far, I’ve been loading instructions into the machine by allowing the Haskell syntax to handle it. Remember, every [ 1, 2, 3 ] :: Cell is actually Cons 1 (Cons 2 (Cons 3 Nil)). Since the whole machine is made of cons-cells, I need to be able to construct new cells via an instruction.

The CONS opcode constructs a new cons cell on the fly from the top two values on the stack:

-- (a:b:s) e (CONS:c) d -> ((a:b):s) e c d
step (Cons a (Cons b s), e, Cons CONS c, d) = ((Cons (Cons a b) s, e, c, d), Ready)

Now, when I run NIL NIL CONS, I get [[]], which is a list, containing a single item that is the empty list.

The CAR opcode selects the first element of a cons-cell. This means that CAR acts as both fst for tuples and head for lists:

-- ((a:b):s) e (CAR:c) d -> (a:s) e c d
step (Cons (Cons a b) s, e, Cons CAR  c, d) = ((Cons a s, e, c, d), Ready)

The CDR opcode selects the second element of a cons-cell. This means that CDR acts as both snd for tuples and tail for lists:

-- ((a:b):s) e (CDR:c) d -> (b:s) e c d
step (Cons (Cons a b) s, e, Cons CDR  c, d) = ((Cons b s, e, c, d), Ready)

Now, if we run the following sequence:

NIL             -- An empty list, []
NIL NIL CONS    -- The second element, [[]]
CONS            -- A list containing the second element, [[[]]]
NIL             -- The first element, []
CONS            -- A list containing the first and second element, [ [], [[]] ]

It results in the top of the stack having the value [ [], [[]] ] which is a list, containing first an empty list and second a singleton list that itself contains an empty list. We can then apply CAR or CDR to choose the first or second list, yielding [] or [[]] respectively

LDC and ATOM

Building things out of lists is not very legible, so let’s start loading some atom / integers instead.

The LDC opcode is very simple, it pops a constant from the control stack, and pushes it onto the stack:

--  s e (LDC:k:c) d => (k:s) e c d
step (s, e, Cons LDC (Cons k c), d) = ((Cons k s, e, c, d), Ready)

So, load [ LDC, x, STOP ] will result in the machine ([], [], [LDC, a, STOP], []) which will immediately transition to ([x], [], [STOP], []) and then halt as ([x], [], [], []). The loaded value is usually an atom, but it can be anything.

The ATOM opcode tells us whether or not a given value is an Atom:

atom :: Cell -> Cell
atom (Atom _) = 1
atom _        = 0

-- (a:s) e ATOM:c d -> ((atom a):s) e c d
step (Cons a s, e, Cons ATOM c, d) = ((Cons (is_atom a) s, e, c, d), Ready)

Thus, [ NIL, ATOM ] pushes a false value 0 onto the stack, and [ LDC, 0, ATOM ] pushes a truth value 1 onto the stack.

Arithmetic

All of the atomic binary ops follow the same pattern:

-- NOTE: These are incomplete pattern matches that should otherwise result in an
-- aborted state but for simplicity we'll ignore that for now and let it crash 
atom_eq (Atom a) (Atom b) = Atom (if a == b then 1 else 0)
atom_leq (Atom a) (Atom b) = Atom (if a <= b then 1 else 0)
atom_add (Atom a) (Atom b) = Atom (a + b)
atom_sub (Atom a) (Atom b) = Atom (a - b)
atom_mul (Atom a) (Atom b) = Atom (a * b)
atom_div (Atom a) (Atom b) = Atom (div a b)
atom_rem (Atom a) (Atom b) = Atom (rem a b)

-- a:b:s e ATOM_BINOP:c d => (op a b):s e c d
step (Cons a (Cons b s), e, Cons EQ   c, d) = ((Cons (atom_eq a b) s,  e, c, d), Ready)
step (Cons a (Cons b s), e, Cons LEQ  c, d) = ((Cons (atom_leq a b) s, e, c, d), Ready)
step (Cons a (Cons b s), e, Cons ADD  c, d) = ((Cons (atom_add a b) s, e, c, d), Ready)
step (Cons a (Cons b s), e, Cons SUB  c, d) = ((Cons (atom_sub a b) s, e, c, d), Ready)
step (Cons a (Cons b s), e, Cons MUL  c, d) = ((Cons (atom_mul a b) s, e, c, d), Ready)
step (Cons a (Cons b s), e, Cons DIV  c, d) = ((Cons (atom_div a b) s, e, c, d), Ready)
step (Cons a (Cons b s), e, Cons REM  c, d) = ((Cons (atom_rem a b) s, e, c, d), Ready)

At last, we can run our first program! If we load our [ LDC, 1, LDC, 2, ADD, STOP ], we should get the following sequence of states:

Initial state.
[] [] [LDC, 1, LDC, 2, ADD, STOP] []
[1] [] [LDC, 2, ADD, STOP] []
[2,1] [] [ADD, STOP] []
[3] [] [STOP] []
Stopped.
[3] [] [] []

Behold, 3!

SEL and JOIN

Running a sequence of commands is great, but now I want some choice!

The SEL opcode is the SECD machine’s branching instruction. It is our most complicated instruction so far, because it both requires a conditional value on the stack, as well as not just one but two trailing opcodes that point to each branch’s control stack. It also causes the current control stack to be pushed onto the dump:

cond :: Cell -> Cell -> Cell -> Cell
cond (Atom 1) tr fl = tr
cond (Atom 0) tr fl = fl
-- Incomplete pattern match

-- (x:s) e (SEL:tr:fl:c) d => s e (cond x tr fl) (c:d)
step (Cons x s, e, Cons SEL (Cons tr (Cons fl c)), d) = ((s, e, cond_sel x tr fl, Cons c d), Ready)

Furthermore, the SEL opcode requires that both branch control sequences end with the JOIN opcode, which pops the old control stack back off the dump and returns to it:

-- s e (JOIN:_) c:d => s e c d
step (s, e, Cons JOIN _, Cons c d) = ((s, e, c, d), Ready)

The instruction sequence [LDC, 0, SEL, [LDC, 99, JOIN], [LDC, 100, JOIN], LDC, 10, ADD, STOP] load a false condition, selects the second branch, loads 100, jumps back, loads 10, and adds it for a final result of 110:

Initial state.
[] [] [LDC, 0, SEL, [LDC, 99, JOIN], [LDC, 100, JOIN], LDC, 10, ADD, STOP] []
[0] [] [SEL, [LDC, 99, JOIN], [LDC, 100, JOIN], LDC, 10, ADD, STOP] []
[] [] [LDC, 100, JOIN] [[LDC, 10, ADD, STOP]]
[100] [] [JOIN] [[LDC, 10, ADD, STOP]]
[100] [] [LDC, 10, ADD, STOP] []
[10,100] [] [ADD, STOP] []
[110] [] [STOP] []
Stopped.
[110] [] [] []

The SECD machine lacks a JMP instruction, but it can easily be implemented using NIL NULL SEL jmp NIL. It also lacks a switch statement, but it would be trivial to implement a SELN that switches based on an integer index instead of pair of boolean cases.

LDF AP RTN and LD

I need to add a something to our Cell type real quick:

data Cell
    = Nil
    | Cons Cell Cell
    ...
    | Clos Control Env -- A closure is just a special cons cell
    ...
    | Atom Int
    | Opcode Opcode

The LDF opcode pops a function body from the control stack, takes the current environment, conses them together into a closure, pushing the closure onto the stack. A Closure is just a special Cons cell, where the first element is the control stack of the function body, and the second element is the enclosing environment that the function runs in. We give it its own constructor for easier bookkeeping.

-- s e (LDF:f:c) d => (<f:e>:s) e c d -- NOTE: <x:y> denotes a closure (x:y)
step (s, e, Cons LDF (Cons fn c), d) = ((Cons (Clos fn e) s, e, c, d), Ready)

Note that LDF doesn’t actually run the function - it just loads the function onto the stack and binds the current environment to it, while you are still in the current environment, so if we run the machine a few steps we get the following state:

[] [e] [LDF, [LDC, 10, STOP], ABRT] []
[<[LDC, 10, STOP],[e]] [e] [ABRT] []
Aborted leaving the closure on the stack.

The next instruction to be run is actually the ABRT because we never called the function.

To actually apply the function, you need the AP opcode.

AP is easily the most complicated opcode. It does the same thing as it does in haskell - it applies a function to its argument. Or rather, a list of arguments, because a SECD function takes its arguments in the form of a list that has been pushed onto the stack immediately before loading the function. This means SECD functions are of the form fn [a,b,c,...] :: [Cell] -> Cell, which is of course just Cell -> Cell but we know that the argument is a list.

Technically SECD functions are always of the form fn :: Cell -> Cell, because [Cell] is just Cell. This places SECD functions as being capable of not just supporting but distinguishing between both curried (single-argument) multi-argument lambdas f a b c :: a -> b -> c -> z and uncurried (list-argument) lambdas f [a,b,c] :: [a,b,c] -> z, where a singleton-list-argument f [a] can be downconverted to the single-argument f a. This could be achieved by adding an AP_ONE instruction to dispense with wrapping it in NIL a CONS, but we can get away upconverting a as [a] instead, by automatically wrapping it in NIL a CONS.

NOTE: Double debruijn levels collapse to regular de bruijn levels when list-argument lambdas get collapsed to single-argument lambdas. So the SECD machine

If you look closely, you can’t try to apply a function to no arguments - even a function with no arguments, still needs a empty list as an argument. So, LDF never gets used alone. It always has a NIL, and maybe some arguments and CONSes.

AP looks like this:

-- (<c':e'>:v:s) e (AP:c) d => [] (v:e') c' (s:e:c:d)
step (Cons (Clos c' e') (Cons v s), e, Cons AP c, d) = ((Nil, Cons v e', c', Cons s (Cons e (Cons c d))), Ready)

In short order, AP does all of the following:

  • Pops a closure <c':e'> from the stack
  • Pops an argument list v from the stack
  • Pushes the current stack, env, and control onto the dump
  • Replaces the old stack with a fresh empty list
  • Replaces the old environment with the closure environment e'
  • Pushes the argument list v onto the closure enviroment
  • Replaces the old control with the closure body c'

This is how variables enter the environment - through being added to the list that gets pushed onto the stack before calling LDF which copies it to the closure environment that gets loaded when we use AP. Just imagine it as if our lambdas were uncurried and took lists of arguments intead

You may notice that the earlier LDF example did not do this. Nothing would have gone wrong because we didn’t try to AP it. If we wanted to call the function properly, we always need a list of arguments to apply it to.

Even without any arguments, we still need to prepend a NIL instruction to give it an empty list to apply to, so the proper sequence for the function ten = 10 aka [LDC, 10, RTN] would be [NIL, LDF, ten, AP, STOP]. This is how to call functions with no arguments, which is supplied via the empty list.

It is a rather simple opcode extension to have an AP_N n function that handles packing the argument list for you, such that x, y, z, LDF, fn, AP_N, 3 is the same as NIL, x, CONS, y, CONS, z, LDF, fn, AP. The SECD machine allows many such optimizations at the cost of inflating the OPCODE table, but they are always compilable back down to the original set of SECD opcodes.

I’ve actually glossed over RTN so lets define that quickly. Its like JOIN, except its used with AP instead of SEL - you always need to end a function with RTN, just like you always need to end a branch with JOIN. The only difference is that RTN also restores the environment, so it has juggle the return result x a little.

-- (x:_) _ (RTN:_) (s:e:c:d) => (x:s) e c d
step (Cons x _, _, Cons RTN _, Cons s (Cons e (Cons c d))) = ((Cons x s, e, c, d), Ready)

All RTN does, is:

  • Pops a single return value from the stack (you should always put something on the stack, or NIL to return nothing)
  • Pops the old control, env, and stack, replacing the function’s context with its calling context
  • Push the return value back onto the stack, moving it from the function to the caller

So, [ NIL, RTN ] returns nothing, [ LDC, 5, RTN ] returns a 5, and [ NIL, LDC, 5, CONS, LDC, 10, CONS, RTN ] returns [10,5]. Note that, unlike how functions take arguments as a single list, functions return results as a single value - which could be a list, but doesn’t have to be.

This seems odd compared to functions always taking a list of arguments, but in a direct mirror to a list of multiple arguments always being a single argument that is a list, a list of multiple results is always a single result that is a list. And we can efficiently place it right on the stack, where we might efficiently hand it as the list-argument to the next function being called. This actually makes where we place lambda slashes mechanically meaningful when converting eg f a b c to f [a,b,c].

If we wanted to actually give it an argument that we can use, we would need to first construct the list by pushing its arguments onto the stack intermixed with NIL and CONS, and by accessing those variables using LD:

-- f x y = x + y
add_two = [LD, Index 0 0, LD, Index 0 1, ADD, RTN]
[ NIL
, LDC, 5    -- y
, CONS
, LDC, 10   -- x
, CONS
, LDF, add_two -- f
, AP    -- f [x,y]
, STOP
]

I’ve also added another constructor to our cell

data Cell
    = Nil
    | Cons Cell Cell
    | Clos Control Env
    ...
    | Index Int Int    -- An environment index is a double-debruijn level
    ...
    | Atom Int
    | Opcode Opcode

The final opcode is LD, which stands for Load environment. Think of it as LDE to match LDC and LDF. This is the first time we’re actually using the environment (I saved it for last) so it bears some explaining.

A SECD machine uses DeBruijn levels (counting from the bottom up, \ x y -> x becomes \ s -> $0), meaning they don’t require variable names, and we don’t need to worry about alpha equivalence.

Except, because a SECD machine uses argument lists, the environment is a list of frames, so it actually uses Double DeBruijn-levels, which perfectly matches indices being encoded as peano numbers. This means we store an index as a pair of numbers, which makes it is just another special Cons, where the car and cdr are always Int, so we skip packing them into an Atom.

There is no opcode for creating an index, they need to be generated during assembly by replacing named references with their respective double-debruijn index. We could easily add an IX opcode to allow this, or allow the Index to just be Cons (Atom b) (Atom n).

Actually loading up an environment value is as simple as indexing into the list of environment frames, and then indexing into the frame’s arguments:

index :: Cell -> Int -> Cell
index (Cons x _)  0 = x
index (Cons _ xs) n = env_index (n - 1) xs
index _ _ = error "Error: index: Malformed stack"

locate :: Cell -> Cell -> Cell
locate e (Index b n) = index (index e b) n
locate _ _ = error "Error: locate: Malformed index"

-- s e (LD:ix:c) d => ((locate e ix):s) e c d
step (s, e, Cons LD (Cons ix@(Index _ _) c), d) = ((Cons (locate e ix) s, e, c, d), Ready)

Then it places the looked up value onto the stack, and viola!

Lets try it out with (\ _ y -> y) 1 99. I’m going to insert some dummy variables so you can track the stack and env more easily. They just give us some outer context without having to define it.

Initial state.
[s] [e] [NIL, LDC, 99, CONS, LDC, 1, CONS, LDF, [LD, Index 0 1, RTN], AP, STOP] []
[[],s] [e] [LDC, 99, CONS, LDC, 1, CONS, LDF, [LD, Index 0 1, RTN], AP, STOP] []
[99,[],s] [e] [CONS, LDC, 1, CONS, LDF, [LD, Index 0 1, RTN], AP, STOP] []
[[99],s] [e] [LDC, 1, CONS, LDF, [LD, Index 0 1, RTN], AP, STOP] []
[1,[99],s] [e] [CONS, LDF, [LD, Index 0 1, RTN], AP, STOP] []
[[1,99],s] [e] [LDF, [LD, Index 0 1, RTN], AP, STOP] []
Loading the function.
[<[LD, Index 0 1, RTN],[e]>,[1,99],s] [e] [AP, STOP] []
Applying the function.
[] [[1,99],e] [LD, Index 0 1, RTN] [[s], [e], [STOP]]
-- Load the second value from the first environment
[99] [[1,99],e] [RTN] [[s], [e], [STOP]]
-- Return it
[99,s] [e] [STOP] []
Stopped.
[99,s] [] [] []

If we wanted to access values from the higher environment e, assuming it is a list of values as [ 5, 10, 15 ], then upon loading the function as earlier, we would have the state:

[] [[1,99],[5,10,15]] [LD, Index 0 1, RTN] [[s], [[5,10,15]], [STOP]]

If we then switched Index 0 1 which selects the second variable in the first environment, with Index 1 0, selecting the first varible of the second enviornment, we would have loaded 5 instead of 99, resulting in the state:

[] [[1,99],[5,10,15]] [LD, Index 1 0, RTN] [[s], [[5,10,15]], [STOP]]
-- Load the first value from the second environment
[5] [[1,99],[5,10,15]] [RTN] [[s], [[5,10,15]], [STOP]]

This is how the SECD machine accesses the outer environment of a closure.

DUM and RAP

DUM and RAP are the letrec to LDF and AP’s let, so they are identical with the exception of placing a PENDING cell (a special Nil) onto the environment stack one level above where the function’s applied arguments go, meaning PENDING becomes the env list accessed by Index 1 _, before then defining the recursive functions in that environment. Then, RAP replaces the PENDING with the real environment fixing the recursive functions, and you can now APply the actual argument list to the fixed recursive function.

It isn’t as easy as this though, for technical reasons - the PENDING cell is the single mutable / lazy SECD machine. Well, not technically mutable or lazy - its more a unique ‘uninitialized’ state that still can exist in a write-once read-many tape machine. We allocate the memory, but skip writing to it until later. Its not unlike blackholing, except there’s not even a thunk being written yet.

I need to swap out the PENDING for the real letrec environment which can only occur after I’ve shoved it in there. And to do that I need to use an IORef and unsafePerformIO or lift step to IO, or use some sort of chronomorphism, and that’s a lot of work that isn’t necessary in Haskell because Haskell definitions already allow recursion:

rec_a = [..., LDF, rec_b, ...]
rec_b = [..., LDF, rec_a, ...]

This is sort of what I meant by, implementing the SECD machine in a functional language is a little pointless aside from as a academic exercise. Also, it does cause things to explode if you try to debug print a recursive closure.

So, I’m not going to discuss implementing DUM and RAP here, I will discuss them in detail in the next article, which will cover a C VM implementation.

Full source

[UNDER CONSTRUCTION]

Conclusion

This post has been a demonstration of a SECD machine running in Haskell. The problem with this implementation, is that it’s backwards. It relies on the laziness of the host language to allocate and manage memory, and to tie recursive knots, and it doesn’t do anything Haskell can’t already do itself.

A SECD machine is intended to be used to implement a functional programming language, which is why it feels redundant to implement it in Haskell - there’s not much point. It is like using GHC to compile lambda calculus and saying “look how lightweight it is”. Yeah, if you ignore the Giant Haskell Compiler hiding behind it.

It needs to be the other way around, with Haskell running in SECD. In the next post, I will demonstrate a C implementation of the SECD machine.

Future plans, big ones

I’ve been doing a lot of writing Haskell in Lisp in SECD in C lately as part of bootstrapping a very small self-hosted Haskell compiler that describes its own memory and runtime in pure Haskell. I’m going to remove layers one by one until we’re left with just pure Haskell, and I’m going to do it with style, and maybe a few, tiny adjustments to the meaning of some core haskell syntax.

Here’s whats coming down the pipeline:

  • I’ve already fused out the Lisp by translating it to Haskell list syntax, and in this post, I’m showing how I’m fusing the SECD opcode into Haskell syntax.
  • Then, by writing a not-exactly-untyped lambda calculus parser in not-exactly-untyped lambda calculus that emits SECD opcode written in Haskell, I can use the parser to close the loop and compile itself down to SECD, leaving me with just Haskell and C.
  • Then, I am going to use memalloc to make the C code disappear, just like I’ve gotten rid of the Lisp and SECD opcodes.
  • The C VM can already be compiled to WASM to run SECD opcode in the browser, but I am going to add support for compiling SECD to WASM directly, since Web Assembly is also a stack machine making it easy to skip the C entirely.
  • This also opens the path for compiling to RISCV, and eventually ARM and X86.

At this point, it should be self-hosted and homoiconic, but I have plans to go further:

  • Then I am going to use botan to introduce code hashing and signing
  • Then, I am going to apply birecursion-schemes to the SECD cell’s base functor, to add runtime source control and turn the LHC into a distributed compiler like if Haskell ate Git as a concept
  • Then, I am going to use the math library to build a distributed game engine riding that compiler.

Then I am going to make a puzzle game that teaches programming.

A teaser for next time, here is the C VM running a simple “hello world” script:

[Loading program]
Machine: READY, 0 steps
S: @0 []
E: @0 []
C: @124 [LDC, 10, LDC, 100, LDC, 108, LDC, 114, LDC, 111, LDC, 119, LDC, 32, LDC, 111, LDC, 108, LDC, 108, LDC, 101, LDC, 104, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, LDC, 2, PUTC, STOP]
D: @0 []
[Running machine]
hello world
[Machine stopped]
Machine: STOPPED, 37 steps
S: @0 []
E: @0 []
C: @0 []
D: @0 []
Yard: 256 cells, high mark @148, first free @149

Its C, but its running SECD code written in valid Haskell syntax!

Sources:

4 Likes
3

Does this ignore the argument?
Also, you can use pattern synonyms to deal with the opcode problem

data Opcode
    = OPABRT -- Non-canonical panic
    -- Constructing cons cells
    | OPNIL
    | OPNULL
    | OPCONS
    | OPCAR
    | OPCDR
    -- Loading constants and variables
    | OPLDC
    | OPLD
    -- Loading and applying functions
    | OPLDF
    | OPAP
    | OPRTN
    -- Branching
    | OPSEL
    | OPJOIN
    -- Recursive contexts
    | OPDUM
    | OPRAP
    -- Atom functions
    | OPATOM
    | OPEQ
    | OPLEQ
    | OPADD
    | OPSUB
    | OPMUL
    | OPDIV
    | OPREM
    -- Stop the program
    | OPSTOP
    -- ... OPCODE EXTENSIONS
pattern ABRT = OPABRT -- ...

You can also use TH to automate this. I’ve used this technique before, but I’m not sure if you would want it, because the value of an Opcode type might be limited.

1 Like
4

Whoops, nice catch - that’s just meant to be load prog = ([], [], prog, []), looks like I missed some renaming. I am still slogging through editing, so there are bound to be a few copy-pasting errors. I am a better programmer than I am a content editor.

Yes! But then, I would have to implement pattern synonyms and TH in my compiler, and the goal is for the compiler to compile itself! I am deliberately sticking with relatively simple Haskell features, just OverloadedLists and TypeFamilies to get access to list syntax. I even have a plan to implement the same functionality as TH by making it first class using homoiconicism and using copy as third evaluation strategy instead of strict or lazy.

1 Like
5

Is it lazy? If so, how?

6

The SECD machine is strict by default, but it is easy to add laziness - just zero-arg-lambda \-> f a a function application to thunk it.

I don’t even need a dummy () argument to call it, because an empty argument list is already Nil - one of the benefits of cons-cells allowing one to represent functions as both f :: a -> b -> ... -> z and f :: [a,b,...] -> z.

7

That would give you call-by-name, not call-by-need. I was just curious if you were aiming to implement a strict or non-strict language.

1 Like
8

At this point it still relies on the host Haskell system, so there’s no difference yet. This is what I meant by it being backwards to implement this in Haskell (using pure functions), but I needed to demonstrate what a SECD machine is in a familiar language before diving into C.

This is why I’ll be explaining DUM and RAP next, which uses a Pending thunk to generate a recursive context, using a mechanism similar to GHC’s blackholing. I’m not entirely sure, but I strongly suspect I can use it to make proper thunks too, just by not being recursive, and even if I can’t, it only needs a little tweaking to make it so.

However, I’d prefer to give thunks a specific THUNK opcode and Thunk Cell Cell constructor anyway (oh look, another cons variant) for better tracking and then give them a specific AP_T opcode or something, but AP_T is really just AP because AP expects a already list, and a thunk just needs Nil.

I could lift step to IO to illustrate DUM and RAP and Pending, and use the Cell a base functor to get Cell Addr and then index into a mutable array of Cell Addr exactly like I do in C, but I haven’t finished my memalloc library yet to make it easy to perform memory-allocating variants of functor map and recursion schemes.

(I am working on a lot, this compiler pulls a lot of threads together)

1 Like