ION.lhs

= The ION machine =

One of the many problems with link:lambda.html[our "ultimate" compiler] is that
we used a rich powerful language based on lambda calculus to build a shoddy
compiler for bare-bones lambda calculus.

Let us begin anew from a lower level.
We take a page from Knuth's _The Art of Computer Programming_ and introduce a
mythical computer: the International Obfuscated Nonce (ION) machine, so named
because it's based on a one-time random design used in link:ioccc.html[an entry
to the 26th International Obfuscated C Code Contest].

The basic unit of data is a 32-bit word. Memory is an array of 32-bit words,
indexed by 32-bit words. Among the registers are the heap pointer HP and the
stack pointer SP. The instruction set consists of the usual suspects: loading
and storing words, arithmetic, jumps. The contents of memory are initially
undefined. We write `Int` for the type of 32-bit words. (Using `Word32`
requires more imports and conversions here and there.)

++++++++++
<script>
function hideshow(s) {
  var x = document.getElementById(s);
  if (x.style.display === "none") {
    x.style.display = "block";
  } else {
    x.style.display = "none";
  }
}
</script>
<p><a onclick='hideshow("ugh");'>&#9654; Toggle extensions and imports</a></p>
<div id='ugh' style='display:none'>
++++++++++

\begin{code}
{-# LANGUAGE NamedFieldPuns #-}
module ION where
import Data.Char (chr, ord)
import qualified Data.Map as M
import Data.Map (Map, (!))
import System.IO
\end{code}

++++++++++
</div>
++++++++++

\begin{code}
data VM = VM { sp :: Int, hp :: Int, mem :: Map Int Int }
\end{code}

We take advantage of native 32-bit words rather than encode numbers in pure
lambda calculus, at the cost of introducing combinators that correspond to
native arithmetic instructions.

Let `n` be a 32-bit word. If `n` lies in [0..127], `n` represents a combinator,
otherwise `n` represents the application of the expression represented by
`load n` to the expression represented by `load (n + 1)`. There is an
exception to this rule: if `load n = 35` (the ASCII code of "#") then `n`
represents the 32-bit constant returned by `load (n + 1)`.

This implies we can never refer to an application held in the first 128 memory
locations, and also implies we have limited ourselves to at most 128 different
combinators.

When possible, combinators are represented by the ASCII code of a related
character. For example, `66` is the B combinator, since `ord 'B' == 66`
and `42` is the multiply combinator, since `ord '*' == 42`.

We initialize HP to 128, the bottom of the heap, which grows upwards.
We set SP to the highest memory address, the bottom of the stack, which
grows downwards. The stack keeps track of where we've been as we walk up and
down the left spine of the tree representing the combinatory logic term being
evaluated.

\begin{code}
new :: VM
new = VM maxBound 128 mempty

load :: Int -> VM -> Int
load k vm = mem vm ! k

store :: Int -> Int -> VM -> VM
store k v vm = vm{mem = M.insert k v $ mem vm}

app :: Int -> Int -> VM -> (Int, VM)
app x y vm@VM{hp} = (hp, store hp x $ store (hp + 1) y $ vm { hp = hp + 2 })

push :: Int -> VM -> VM
push n vm@VM{sp} = store (sp - 1) n $ vm{sp = sp - 1}
\end{code}

== Sharing economy ==

We earlier noted that applying the S combinator causes two nodes to refer to
the same subterm. This sharing saves room, but we can save more.

Suppose two nodes X and Y point to the same subterm T. On reducing X, our
`reduce` function created a new subterm U, and changed X to point to U and
left Y pointing to T (reminiscent of copy-on-write).

Instead, we should simply replace T with U so that reducing either one of X
or Y causes both to point to U afterwards. This strategy is known as _lazy
evaluation_, and our `lazy` function below carries it out.

Even though the result is the same, we see this order as different to normal
order, because we reduce both X and Y (and possibly other nodes) even if they
are not the two left-most subterms.

The tacit application of `load n` to `load (n + 1)` creates complications
with lazy evaluation, which we work around with the aid of the identity
combinator. For example, if an application evaluates to `K`, then we replace
it with `IK`.

== The numbers game ==

For primitive functions, we use a trick described in depth by Naylor and
Runciman, _The Reduceron reconfigured and re-evaluated_: we introduce a
combinator called `+#+` and reduce, say, `+# 42 f+` to `+f(# 42)+` for any `f`.
For example, the term `+++(I#2)(K(#3)S)(+))+++` reduces to `+++(+)(#3)(#2)+++`.

In this fashion, the first two arguments of `(+)` are always primitive
integers, so our code for reducing `(+)(#m)(#n)` simply pulls out the words `m`
and `n` from certain locations in memory and returns `#s` where `s == m + n`
modulo 2^32^.

This scheme resembles the approach described by Peyton Jones and Launchbury,
_Unboxed values as first class citizens in a non-strict function language_.
For example, they define integer subtraction as follows:

------------------------------------------------------------------------
(-) p q = case p of
  Int p# -> case q of
    Int q# -> case (p# -# q#) of
      t# -> Int t#
------------------------------------------------------------------------

After Scott-encoding, we have:

------------------------------------------------------------------------
(-) p q = p (\p# -> q(\q# -> (p# -# q#) \t# -> Int t#))
------------------------------------------------------------------------

In other words, using their notation, `42 f` reduces to `f(42#)`. However, our
subtraction operator also boxes the result, while they have a separate boxing
step, which is better for optimization. We may wish to follow suit and split
off boxing, though it likely means introducing supercombinators to reap the
benefits.

We support the operations `+ - / * % = L`. The first 5 have the same meaning
they do in C, while the last 2 are equivalent to C's `+(==)+` and `+(<=)+`.

We add a couple of useful macros: the `R` combinator (equivalent to `CC`) and
the `(:)` combinator (equivalent to `B(BK)(BCT)`).

Below, the I combinator is not lazy: for instance, every time we encounter the
subterm `I(I(Ix))` we must reduce three I combinators. link:ioccc.html[The
competition version of this code] does lazily evaluate `I` combinators, but
consequently treads carefully near the top of the stack.

\begin{code}
arg' :: Int -> VM -> Int
arg' n vm = load (load (sp vm + n) vm + 1) vm

arg :: Int -> VM -> (Int, VM)
arg n vm = (arg' n vm, vm)

app' :: (VM -> (Int, VM)) -> (VM -> (Int, VM)) -> VM -> (Int, VM)
app' f g vm = let
  (x, vm1) = f vm
  (y, vm2) = g vm1
  in app x y vm2

apparg :: Int -> Int -> VM -> (Int, VM)
apparg m n vm = app (arg' m vm) (arg' n vm) vm

wor n = (,) n
com = wor . ord

lazy n f g vm = let
  (p, vm1) = f vm
  (q, vm2) = g vm1
  dst = load (sp vm + n) vm
  in store dst p (store (dst + 1) q vm2) { sp = sp vm + n}

numberArg n vm = load (fst (arg n vm) + 1) vm

builtin :: Int -> VM -> VM
builtin c vm = case chr c of
  'I' -> store (sp vm + 1) (fst $ arg 1 vm) vm { sp = sp vm + 1 }
  'K' -> lvm 2 (com 'I') (arg 1)
  'Y' -> lvm 1 (arg 1) (wor $ load (sp vm + 1) vm)
  'T' -> lvm 2 (arg 2) (arg 1)
  'S' -> lvm 3 (apparg 1 3) (apparg 2 3)
  'B' -> lvm 3 (arg 1) (apparg 2 3)
  'C' -> lvm 3 (apparg 1 3) (arg 2)
  'R' -> lvm 3 (apparg 2 3) (arg 1)
  '#' -> lvm 2 (arg 2) (wor $ load (sp vm + 1) vm)
  ':' -> lvm 4 (apparg 4 1) (arg 2)
  '=' | num 1 == num 2 -> lvm 2 (com 'I') (com 'K')
      | otherwise      -> lvm 2 (com 'K') (com 'I')
  'L' | num 1 <= num 2 -> lvm 2 (com 'I') (com 'K')
      | otherwise      -> lvm 2 (com 'K') (com 'I')
  '*' -> lvm 2 (com '#') (wor $ num 1 * num 2)
  '+' -> lvm 2 (com '#') (wor $ num 1 + num 2)
  '-' -> lvm 2 (com '#') (wor $ num 1 - num 2)
  '/' -> lvm 2 (com '#') (wor $ num 1 `div` num 2)
  '%' -> lvm 2 (com '#') (wor $ num 1 `mod` num 2)
  '?' -> error "?"
  where
  num n = numberArg n vm
  lvm n f g = lazy n f g vm
\end{code}

== ION I/O ==

For us, a program `P` is a function from a string to a string, where strings
are Scott-encoded lists of characters.

To run `P` on standard input and output, we initialize the VM with
`P(0?)(.)(T1)` then repeatedly reduce until asked to reduce the `(.)`
combinator.

The `0` combinator takes one argument, say `x`. The term `0x` reduces to `IK`
at the end of input or `(:)(#c)(0?)` where `c` is the next input character.
The unused argument `x` is a consequence of the ION machine's peculiar encoding
of applications and the need to ensure there is at most one `0` combinator
in the heap.

The `1` combinator takes two arguments, say `x` and `y`. The first argument `x`
should be an integer constant, that is, `#c` for some `c`. Then the character
with ASCII code `c` is printed on standard output, and the expression
`1xy` is reduced to `y(.)(T1)`.

(In ION assembly, symbols, letters and digits are just names of combinators. In
particular, the `(.)` combinator is not a binary operator representing function
composition. Similarly, `0` and `1` do not represent integers; the names of
these combinators were inspired by the file descriptors of standard input and
output.)

\begin{code}
eval :: Monad m => (Int -> VM -> m (Maybe VM)) -> VM -> m VM
eval exts vm@VM{sp} = let n = load sp vm in
  if n >= 128 then eval exts $ store (sp - 1) (load n vm) vm { sp = sp - 1 }
  else if n == ord '.' then pure vm
  else eval exts =<< (maybe (builtin n vm) id <$> exts n vm)

extsIO :: Int -> VM -> IO (Maybe VM)
extsIO n vm = case chr n of
  '0' -> do
    b <- isEOF
    if b then lvm 1 (com 'I') (com 'K')
    else do
      c <- getChar
      lvm 1 (app' (com ':') (app' (com '#') (com c))) (app' (com '0') (com '?'))
  '1' -> do
    putChar $ chr $ numberArg 1 vm
    lvm 2 (app' (arg 2) (com '.')) (app' (com 'T') (com '1'))
  _ -> pure Nothing
  where
  lvm n f g = pure $ Just $ lazy n f g vm

evalIO :: VM -> IO VM
evalIO = eval extsIO
\end{code}

== Machine shop ==

https://www.youtube.com/watch?v=zhj_tUMwTe0[Edward Kmett's talk _Combinators Revisited_] contains many relevant references and ideas.

Other choices for implementing lambda calculus include:

  * https://en.wikipedia.org/wiki/SECD_machine[SECD machine]
  * https://en.wikipedia.org/wiki/Krivine_machine[Krivine machine]
  * http://matt.might.net/articles/cek-machines/[CEK machine]
  * https://www.microsoft.com/en-us/research/publication/implementing-functional-languages-a-tutorial/[G-machine; TIM machine] (Chapters 3 and 4)
  * https://www.microsoft.com/en-us/research/wp-content/uploads/1992/04/spineless-tagless-gmachine.pdf[Spineless Tagless G-machine]
  * https://github.com/grin-compiler/grin[GRIN: Graph Reduction Intermediate Notation]