A Combinatory Compiler

The compiler below accepts a Turing-complete language and produces WebAssembly. The source should consist of lambda calculus definitions including a function main that outputs a Church-encoded integer.

intermediate form:

wasm:

LC and CL

We define a data structure that holds both lambda terms and combinators composed exclusively of S and K.

A single data structure is convenient but unclean, as we depend on the user to avoid using "s" and "k" as variable names, and assume the Lam data constructor is unused after bracket abstraction.

infixl 5 :@
data Expr = Expr :@ Expr | Var String | Lam String Expr deriving Eq

instance Show Expr where
  showsPrec p = \case
    Var s -> (s++)
    x :@ y -> showParen (p == 1) $ shows x . showsPrec 1 y
    Lam s x -> showParen True $ ('\\':) . (s++) . ('.':) . shows x

Parser

We build off our lambda calculus parser:

jsEval "curl_module('../compiler/Charser.ob')"

import Charser

source :: Charser [(String, Expr)]
source = foldr ($) [] <$> many maybeLet where
  maybeLet = between ws newline $ ((:) .) . (,) <$> v <*> (str "=" >> term) <|> pure id
  term = lam <|> app
  lam = flip (foldr Lam) <$> between lam0 lam1 (some v) <*> term where
    lam0 = str "\\" <|> str "\955"
    lam1 = str "->" <|> str "."
  app = foldl1 (:@) <$> some
    ((Var <$> v) <|> between (str "(") (str ")") term)
  v   = some alphaNumChar <* ws
  str = (*> ws) . string
  ws = many (char ' ') *> (string "--" *> many (noneOf "\n") <|> pure "")

Let’s test it:

parse source "" [r|
true = \x y -> x
Y = \f -> (\x -> x x)(\x -> f(x x))
|]

Combinators

We recap a smidgeon of combinatory logic. Define the combinators:

\(S = \lambda x y z . x z (y z)\)
\(K = \lambda x y . x\)

The classic bracket abstraction algorithm with the K-optimization is:

\[\begin{align} \lceil \lambda x . M \rceil &= K M \quad (x \notin M) \\ \lceil \lambda x . x \rceil &= S K K \\ \lceil \lambda x . M N \rceil &= S \lceil \lambda x . M \rceil \lceil \lambda x . N \rceil \end{align}\]

Any closed lambda term can be rewritten in terms of \(S\) and \(K\) by applying the above rules starting from the innermost lambda abstraction and working outwards:

lacks x t = case t of
  Var s | s == x -> False
  u :@ v -> lacks x u && lacks x v
  _ -> True

babs0 env = \case
  Var s -> maybe (Var s) (babs0 env) $ lookup s env
  m :@ n -> babs0 env m :@ babs0 env n
  Lam x e -> elimX $ babs0 env e where
    elimX t
      | lacks x t   = Var "k" :@ t
      | otherwise   = case t of
        Var y  -> Var "s" :@ Var "k" :@ Var "k"
        m :@ n -> Var "s" :@ elimX m :@ elimX n

map (second $ babs0 []) <$> parse source "" [r|
true = \x y -> x
Y = \f -> (\x -> x x)(\x -> f(x x))
|]

We also mentioned David Turner found more optimizations, enough to make bracket abstraction practical. However, he used more combinators than just \(S\) and \(K\). Luckily, John Tromp ported the rules to \(S\) and \(K\):

babs env = \case
  Var s -> maybe (Var s) (babs env) $ lookup s env
  m :@ n -> babs env m :@ babs env n
  Lam x e -> go $ babs env e where
    go t
      | Var "s" :@ Var "k" :@ _ <- t = Var "s" :@ Var "k"
      | lacks x t = Var "k" :@ t
      | Var y <- t, x == y  = Var "s" :@  Var "k" :@ Var "k"
      | m :@ Var y <- t, x == y, lacks x m = m
      | Var y :@ m :@ Var z <- t, x == y, x == z =
        go $ Var "s" :@ Var "s" :@ Var "k" :@ Var x :@ m
      | m :@ (n :@ l) <- t, isComb m, isComb n =
        go $ Var "s" :@ go m :@ n :@ l
      | (m :@ n) :@ l <- t, isComb m, isComb l =
        go $ Var "s" :@ m :@ go l :@ n
      | (m :@ l) :@ (n :@ l') <- t, l == l', isComb m, isComb n =
        go $ Var "s" :@ m :@ n :@ l
      | m :@ n <- t = Var "s" :@ go m :@ go n

isComb = \case
  Var x -> elem x ["s", "k"]
  u :@ v -> isComb u && isComb v

map (second $ babs []) <$> parse source "" [r|
true = \x y -> x
Y = \f -> (\x -> x x)(\x -> f(x x))
|]

We assume we have no recursive let definitions and that s and k are reserved keywords.

A few lines in the Either monad glues together the parser and bracket abstraction.

toSK s = do
  env <- parse source "" (s ++ "\n")
  case lookup "main" env of
    Nothing -> Left $ error "missing main"
    Just t -> pure $ babs env t :@ Var "u" :@ Var "z"

We’ve introduced two more combinators: u and z, which we think of as the successor function and zero respectively. Given a Church encoding M of an integer n, the expression Muz evaluates to u(u(…u(z)…)), where there are n occurrences of u. We make u increment a counter, and we make z return it, so when evaluated in normal order it returns n.

Graph Reduction

We encode the tree representing our program into an array, then write WebAssembly to manipulate this tree. In other words, we model computation as graph reduction.

We view linear memory as an array of 32-bit integers. The values 0-3 represent leaf nodes z,u,k,s in that order, while any other value n represents an internal node with children represented by the 32-bit integers stored in linear memory at n and n + 4.

We encode the tree so that address 4 holds the root of the tree. Since 0 represents a leaf node, the first 4 bytes of linear memory cannot be addressed, so their contents are initialized to zero and ignored.

toArr n (Var "z") = [0]
toArr n (Var "u") = [1]
toArr n (Var "k") = [2]
toArr n (Var "s") = [3]
toArr n (x@(Var _) :@ y@(Var _)) = toArr n x ++ toArr n y
toArr n (x@(Var _) :@ y)         = toArr n x ++ [n + 2] ++ toArr (n + 2) y
toArr n (x         :@ y@(Var _)) = n + 2 : toArr n y ++ toArr (n + 2) x
toArr n (x         :@ y)         = [n + 2, nl] ++ l ++ toArr nl y
  where l  = toArr (n + 2) x
        nl = n + 2 + length l
encodeTree :: Expr -> [Int]
encodeTree e = concatMap f $ 0 : toArr 4 e where
  f n | n < 4     = [n, 0, 0, 0]
      | otherwise = toU32 $ (n - 3) * 4
toU32 = take 4 . byteMe
byteMe n | n < 256   = n : repeat 0
         | otherwise = n `mod` 256 : byteMe (n `div` 256)

Our run function takes the current and a stack of addresses state of linear memory, and simulates what our assembly code will do.

For the z combinator, we return 0. For the u combinator we return 1 plus the result of evaluating its argument. For the k combinator, we pop off the last two stack elements and push the evaluation of its first argument.

For s we create two internal nodes representing xz and yz on the the heap hp, where x,y,z are the arguments of s. Then we lazily evaluate: we rewrite the immediate children of the parent of the z node to apply the first of the newly created nodes to the other.

For internal nodes, we push the first child on the stack then recurse.

We assume the input program is well-formed, that is, every k is given exactly 2 arguments, every s is given exactly 3 arguments, and so on.

jsEval "curl_module('../compiler/Map.ob')"

import Map

run m (p:sp) = case p of
  0 -> 0
  1 -> 1 + run m (arg 0 : sp)
  2 -> run m $ arg 0 : drop 2 sp
  3 -> run m' $ hp:drop 2 sp where
    m' = insList m $
      zip [hp..]    (concatMap toU32 [arg 0, arg 2, arg 1, arg 2]) ++
      zip [sp!!2..] (concatMap toU32 [hp, hp + 8])
    hp = size m
  _ -> run m $ get p:p:sp
  where
  arg k = get (sp!!k + 4)
  get n = sum $ zipWith (*) ((m !) <$> [n..n+3]) ((256^) <$> [0..3])
  insList = foldr (\(k, a) m -> insert k a m)

Machine Code

WebAssembly uses LEB128 liberally, as well as length-prefixing. (This clashes slightly, as LEB128 can be thought of as a format using a terminator.)

leb128 n | n < 64   = [n]
         | n < 128  = [128 + n, 0]
         | otherwise = 128 + (n `mod` 128) : leb128 (n `div` 128)
varlen xs = leb128 $ length xs
lenc xs = varlen xs ++ xs
encStr s = lenc $ ord <$> s
encSig ins outs = typeFunc : lenc ins ++ lenc outs where typeFunc = 0x60
sect t xs = t : lenc (varlen xs ++ concat xs)

We mechanically follow the wasm format:

compile :: [Int] -> [Int]
compile heap = let
  typeI32  = 0x7f
  br       = 0xc
  getlocal = 0x20
  setlocal = 0x21
  teelocal = 0x22
  i32load  = 0x28
  i32store = 0x36
  i32const = 0x41
  i32add   = 0x6a
  i32sub   = 0x6b
  i32mul   = 0x6c
  i32shl   = 0x74
  i32shr_s = 0x75
  i32shr_u = 0x76
  i64const = 0x42
  i64store = 0x37
  i64shl   = 0x86
  i64add   = 0x7c
  i64load32u    = 0x35
  i64extendui32 = 0xac
  nPages = 8
  in concat [
  [0, 0x61, 0x73, 0x6d, 1, 0, 0, 0],  -- Magic string, version.
  -- Type section.
  sect 1 [encSig [typeI32] [], encSig [] []],
  -- Import section.
  -- [0, 0] = external_kind Function, index 0.
  sect 2 [encStr "i" ++ encStr "f" ++ [0, 0]],
  -- Function section.
  -- [1] = Type index.
  sect 3 [[1]],
  -- Memory section.
  -- 0 = no-maximum
  sect 5 [[0, nPages]],
  -- Export section.
  -- [0, 1] = external_kind Function, index 1.
  sect 7 [encStr "e" ++ [0, 1]],
  -- Code section.
  -- Locals
  let
    sp = 0  -- stack pointer
    hp = 1  -- heap pointer
    ax = 2  -- accumulator
  in sect 10 [lenc $ [1, 3, typeI32,
    -- SP = 65536 * nPages - 4
    -- [SP] = 4
    i32const] ++ leb128 (65536 * nPages - 4) ++ [teelocal, sp,
    i32const, 4, i32store, 2, 0,
    i32const] ++ varlen heap ++ [setlocal, hp,
    3, 0x40,  -- loop
    2, 0x40,  -- block 4
    2, 0x40,  -- block 3
    2, 0x40,  -- block 2
    2, 0x40,  -- block 1
    2, 0x40,  -- block 0
    getlocal, sp, i32load, 2, 0,
    0xe,4,0,1,2,3,4, -- br_table
    0xb,  -- end 0
-- Zero.
    getlocal, ax, 0x10, 0,  -- call function 0
    br, 5,  -- br function
    0xb,  -- end 1
-- Successor.
    getlocal, ax, i32const, 1, i32add, setlocal, ax,
    -- SP = SP + 4
    -- [SP] = [[SP] + 4]
    getlocal, sp, i32const, 4, i32add, teelocal, sp,
    getlocal, sp, i32load, 2, 0, i32load, 2, 4, i32store, 2, 0,
    br, 3,  -- br loop
    0xb,  -- end 2
-- K combinator.
    -- [SP + 8] = [[SP + 4] + 4]
    getlocal, sp,
    getlocal, sp, i32load, 2, 4, i32load, 2, 4,
    i32store, 2, 8,
    -- SP = SP + 8
    getlocal, sp, i32const, 8, i32add, setlocal, sp,
    br, 2,  -- br loop
    0xb,  -- end 3
-- S combinator.
    -- [HP] = [[SP + 4] + 4]
    -- [HP + 4] = [[SP + 12] + 4]
    getlocal, hp,
    getlocal, sp, i32load, 2, 4, i64load32u, 2, 4,
    getlocal, sp, i32load, 2, 12, i64load32u, 2, 4,
    i64const, 32, i64shl, i64add, i64store, 3, 0,
    -- [HP + 8] = [[SP + 8] + 4]
    -- [HP + 12] = [HP + 4]
    getlocal, hp,
    getlocal, sp, i32load, 2, 8, i64load32u, 2, 4,
    getlocal, hp, i64load32u, 2, 4,
    i64const, 32, i64shl, i64add, i64store, 3, 8,
    -- SP = SP + 12
    -- [[SP]] = HP
    -- [[SP] + 4] = HP + 8
    getlocal, sp, i32const, 12, i32add, teelocal, sp,
    i32load, 2, 0,
    getlocal, hp, i64extendui32,
    getlocal, hp, i32const, 8, i32add,
    i64extendui32, i64const, 32, i64shl, i64add, i64store, 3, 0,
    -- HP = HP + 16
    getlocal, hp, i32const, 16, i32add, setlocal, hp,
    br, 1,  -- br loop
    0xb,  -- end 4
-- Application.
    -- SP = SP - 4
    -- [SP] = [[SP + 4]]
    getlocal, sp, i32const, 4, i32sub,
    teelocal, sp, getlocal, sp, i32load, 2, 4, i32load, 2, 0, i32store, 2, 0,
    br, 0,
    0xb,    -- end loop
    0xb]],  -- end function
  -- Data section.
  sect 11 [[0, i32const, 0, 0xb] ++ lenc heap]]

We’ve manually converted the run function to machine code. Initially, our tree is encoded at the bottom of the linear memory, and the stack pointer is at the top. Some features of WebAssembly may surprise those who accustomed to other instruction sets:

Load and store instructions must be given alignment and offset arguments.
There are no explicit labels or jumps. Instead, labels are implicitly defined by declaring well-nested block-end and loop-end blocks, and branch statements break out a given number of blocks.

The data section initializes the linear memory so our encoded tree sits at the bottom.

To keep the code simple, we ignore garbage collection. Because we represent numbers in unary, and also because we only ask for a few pages of memory, our demo only works on relatively small programs.

User Interface

For the demo, we add a couple of helpers to show the intermediate form and assembly opcodes.

dump asm = unwords $ xxShow <$> asm where
  xxShow c = reverse $ take 2 $ reverse $ '0' : showHex c ""

hexDigit n
  | n <= 9 = chr $ n + 48
  | otherwise = chr $ n + 97 - 10
showHex c = (hexDigit q:) . (hexDigit r:) where (q, r) = divMod c 16

demo = do
  s <- jsEval "input.value;"
  case toSK s of
    Left err -> jsEval $ "sk.value = `error: " ++ show err ++ "`;"
    Right sk -> do
      let asm = compile $ encodeTree sk
      jsEval $ "sk.value = `" ++ show sk ++ "`;"
      jsEval $ "asm.value = `" ++ dump asm ++ "`;"
      jsEval $ "runWasmInts(" ++ show asm ++ ");"

jsEval "initDemo(repl);"

Ben Lynn blynn@cs.stanford.edu 💡