quest.lhs

= Compiler Quest =

Bootstrapping a compiler is like a role-playing game. From humble beginnings,
we painstakingly cobble together a primitive, hard-to-use compiler whose only
redeeming quality is that it can build itself.

Because the language supported by our compiler is so horrible, we can only
bear to write a few incremental improvements. But once we persevere, we
compile the marginally better compiler to gain a level.

Then we iterate. We add more features to our new compiler, which is easier
thanks to our most recent changes, then compile again, and so on.

== Parenthetically ==

Our first compiler converts parenthesized combinatory logic terms to ION
assembly. For example:

------------------------------------------------------------------------
parse "BS(BB);Y(B(CS)(B(B(C(BB:)))C));"
  ==  "``BS`BB;`Y``B`CS``B`B`C``BB:C;"
------------------------------------------------------------------------

We assume the input is valid and uses `@` to refer to previous terms and `#`
for integer constants.

In Haskell we could write:

------------------------------------------------------------------------
term kon acc s = case s of
  h:t
    | h == ')' || h == ';' -> kon acc t
    | h == '('             -> term comp Nothing t
    | otherwise -> (if h == '#' || h == '@' then esc else id) app (h:) t
  where
  app f t = term kon (Just $ maybe id (('`':) .) acc . f) t
  comp m t = maybe undefined (flip app t) m

esc g f t = case t of th:tt -> g (f . (th:)) tt

parse "" = ""
parse s = term (\p t -> maybe id id p $ ';':parse t) Nothing s
------------------------------------------------------------------------

We employ continuation-passing style. Typically, a function might return a pair
consisting of the tree parsed so far and the remainder of the string to parse,
and another function scrutinizes the pair and processes its contents. We fuse
these steps, obtaining shorter code.

To translate to combinatory logic, we break our code into more digestible
pieces and try to order arguments to reduce term sizes (via
https://crypto.stanford.edu/~blynn/lambda/bohm.html[eta-equivalence]). We add
some glue so our code works in GHC.

------------------------------------------------------------------------
eq a b x y = if a == b then x else y
fix f = f (fix f)
cons = (:)
b = (.)
lst t x y = case t of {[] -> x; h:t -> y h t}
must f s = case s of {[] -> undefined; h:t -> f h t}

orChurch f g x y = f x (g x y)
isPre h = orChurch (eq '#' h) (eq '@' h)
closes h = orChurch (eq ';' h) (eq ')' h)
app rkon acc f t = rkon (Just (b (maybe id (b (cons '`')) acc) f)) t
esc g f t = must (\th tt -> g (b f (cons th)) tt) t
atom h gl t = isPre h esc id gl (cons h) t
comp gl a t = maybe undefined (flip gl t) a
sub r gl t = r (comp gl) Nothing t
more r h gl t = eq '(' h (sub r) (atom h) gl t
switch r kon h a t = closes h kon (b (more r h) (app (r kon))) a t
term = fix (\r kon acc s -> must (\h t -> switch r kon h acc t) s)
parseNonEmpty r s = term (\p t -> maybe id id p (cons ';' (r t))) Nothing s
parse = fix (\r s -> lst s "" (\h t -> parseNonEmpty r s))
------------------------------------------------------------------------

We implement Church booleans. For lists, deleting the `lst` call makes the
code appear to use Scott-encoded lists. We could have acted similarly for
`Maybe`, but we save a few bytes with `must` and `maybe`: since we may
substitute anything we like for `undefined`, we compile each of `maybe
undefined`, `maybe id`, and `must` to `C(TI)`.

https://crypto.stanford.edu/~blynn/lambda/kiselyov.html[Bracket abstraction]
yields:

----------------------------------------------------------------
must = C(T I)
orChurch = B S(B B)
isPre = S(B orChurch(eq ##))(eq #@)
closes = S(B orChurch(eq #;))(eq #))
app = R(B(B Just)(B b(must(b(cons #`)))))(B B B)
esc = B(B must)(R(R cons(B B b))(B B B))
atom = S(B C(R id(R esc isPre))) cons
comp = B C(B(B must) flip)
sub = B(R Nothing)(R comp B)
more = R atom(B S(B(C(eq #()) sub))
switch = B(S(B S(C closes)))(S(B B(B C(B(B b) more)))(B app))
term = Y(B(B(B must))(B(B C) switch))
parseNonEmpty = R Nothing(B term(B(C(B B(must id)))(B(cons #;))))
parse = Y(B(S(T K))(B(B K)(B(B K) parseNonEmpty)))
----------------------------------------------------------------

Next, we:

  * Rewrite with prefix notation for application
  * Replace `id const flip cons eq Nothing` with combinators `I K C : =`.
  * Scott-encode `Nothing` and `Just` as `K` and `BKT`.
  * Refer to the nth function with `@` followed by ASCII code n + 31.

------------------------------------------------------------------------
`C`TI;
``BS`BB;
``S``B@!`=##`=#@;
``S``B@!`=#;`=#);
``R``B`B``BKT``BB`@ `B`:#```BBB;
``B`B@ ``R``R:``BBB``BBB;
``S``BC``RI``R@%@":;
``BC``B`B@ C;
``B`RK``R@'B;
``R@&``BS``B`C`=#(@(;
``B`S``BS`C@#``S``BB``BC``B`BB@)`B@$;
`Y``B`B`B@ ``B`BC@*;
``RK``B@+``B`C``BB`@ I`B`:#;;
`Y``B`S`TK``B`BK``B`BK@,;
------------------------------------------------------------------------

We added a newline after each semicolon for clarity; these must
be removed before feeding.

== Exponentially ==

Our next compiler rewrites lambda expressions as combinators using the
straightforward bracket abstraction algorithm we described earlier.

Parsing is based on functions of type:

------------------------------------------------------------------------
type Parser x = [Char] -> Maybe (x, [Char])
------------------------------------------------------------------------

A `Parser x` tries to parse the beginning of a given string for a value of
type `x`. If successful, it returns `Just` the value along with the unparsed
remainder of the input string. Otherwise it returns `Nothing`.

Values of type `Parser x` compose in natural ways. See
http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-044.pdf[Swierstra,
_Combinator Parsing: A Short Tutorial_].

------------------------------------------------------------------------
pure x inp = Just (P x inp);
bind f m = m Nothing (\x -> x f);
(<*>) x y = \inp -> bind (\a t -> bind (\b u -> pure (a b) u) (y t)) (x inp);
(<$>) f x = pure f <*> x;
(*>) p q = (\_ x -> x) <$> p <*> q;
(<*) p q = (\x _ -> x) <$> p <*> q;
(<|>) x y = \inp -> (x inp) (y inp) Just;
------------------------------------------------------------------------

These turn into:

------------------------------------------------------------------------
pure = B(B(BKT))(BCT)
bind = B(C(TK))T;
ap = C(BB(B bind (C(BB(B bind (B pure))))));
fmap = B ap pure;
(*>) = B ap (fmap (KI));
(<*) = B ap (fmap K);
(<|>) = B(B(R(BKT)))S;
------------------------------------------------------------------------

where we have inlined `Just = BKT` and `(,) = BCT`, and use the aliases
`ap = (<*>)` and `fmap = (<$>)`.

I toyed with replacing `Maybe` and pairs with continuations, for example:

----------------------------------------------------------------
pure x s kon1 kon2 = kon2 x s
(<*>) f x s kon1 kon2 = f s kon1 (\g t -> x t kon1 (\y u -> kon2 (g y) u))
(<|>) f g s kon1 kon2 = f s (g s kon1 kon2) kon2
sat f s kon1 kon2 = lst s kon1 (\h t -> f h (kon2 h t) kon1)
----------------------------------------------------------------

but these seem to produce large combinatory logic terms.

Our syntax tree goes into the following data type:

------------------------------------------------------------------------
data Ast = R ([Char] -> [Char]) | V Char | A Ast Ast | L Char Ast
------------------------------------------------------------------------

The `R` stands for "raw", and its field passes through unchanged during
bracket abstraction. Otherwise we have a lambda calculus that supports
one-character variable names. Scott-encoding yields:

------------------------------------------------------------------------
dR s   = \a b c d -> a s;
dV v   = \a b c d -> b v;
dA x y = \a b c d -> c x y;
dL x y = \a b c d -> d x y;
------------------------------------------------------------------------

which translates to:

------------------------------------------------------------------------
dR = B(BK)(B(BK)(B(BK)T));
dV = BK(B(BK)(B(BK)T));
dA = B(BK)(B(BK)(B(B(BK))(BCT)));
dL = B(BK)(B(BK)(B(BK)(BCT)));
------------------------------------------------------------------------

The `sat` parser combinator parses a single character that satisfies a given
predicate. The `char` specializes this to parse a given character, and
`var` accepts any character except the semicolon and closing parenthesis.
We use `sat (const const)` to accept any character, and with that, we can
parse a lambda calculus expression such as `\x.(\y.Bx)`:

------------------------------------------------------------------------
sat f inp = inp Nothing (\h t -> f h (pure h t) Nothing);
char c = sat (\x -> x((==)c));
var = sat (\c -> flip (c((==)';') || c((==)')')));
pre = (.) . cons <$> (char '#' <|> char '@') <*> (cons <$> sat (const const))
atom r = (char '(' *> (r <* char ')')) <|> (char '\\' *> (L <$> var) <*> (char '.' *> r)) <|> (R <$> pre) <|> (V <$> var);
apps r = (((&) <$> atom r) <*> ((\vs v x -> vs (A x v)) <$> apps r)) <|> pure id;
expr = ((&) <$> atom expr) <*> apps expr;
------------------------------------------------------------------------

As combinators, we have:

------------------------------------------------------------------------
sat = B(C(TK))(B(B(RK))(C(BS(BB))pure));
char = B sat(BT=);
var = sat(BC(S(B(BS(BB))(=#;))(=#))))
pre = ap(fmap(BB:)((<|>)(char##)(char#@)))(fmap:(sat(KK)));
atom = C(B(<|>)(C(B(<|>)(S(B(<|>)(B((*>)(char#())(C(<*)(char#)))))(B(ap((*>)(char#\)(fmap dL var)))((*>)(char#.)))))(fmap dR pre)))(fmap dV var);
apps = Y(B(R(pure I))(B(B(<|>))(B(S(B ap(B(fmap T)atom)))(B(fmap(C(BBB)(C dA)))))));
expr = Y(S(B ap(B(fmap T)atom))apps);
------------------------------------------------------------------------

where we have inlined the Church-encoded OR function `BS(BB)`.

The `babs` and `unlam` functions perform simple bracket abstraction, and
`shows` writes the resulting lambda-free `Ast` in ION assembly.

------------------------------------------------------------------------
vCheck f x = f x (V 'I') (A (V 'K') (V x))
unlam caseV = fix (\r t -> t (\x -> A (V 'K') (R x)) caseV (\x y -> A (A (V 'S') (r x)) (r y)) undefined)
babs = fix (\r t -> t R V (\x y -> A (r x) (r y)) (\x y -> unlam (vCheck (x ==)) (r y)))
------------------------------------------------------------------------

Putting it all together, `main` parses as many semicolon-terminated
expressions as it can and converts them to ION assembly.

------------------------------------------------------------------------
main s = (expr <* char ';') s id (\p -> p (\x t -> shows (babs x) . (';':) . main t)) "";
------------------------------------------------------------------------

These last few functions are:

------------------------------------------------------------------------
shows = Y(B(R?)(B(C(R:(TI)))(S(BC(B(BB)(B(BB)(B(B(:#`))))))I)));
vCheck = R(B(dA(dV#K))dV)(BS(R(dV#I)))
unlam = BY(B(B(R?))(R(S(BC(B(BB)(B(B dA)(B(dA(dV#S))))))I)(BB(BC(C(T(B(dA(dV#K))dR)))))));
babs = Y(S(BC(B(C(R dV(T dR)))(S(BC(B(BB)(B dA)))I)))(C(BB(B unlam (B vCheck =)))));
main = RK(Y(B(C(RI((<*)expr(char#;))))(BT(C(BB(BB(R(:#;)(BB(B shows babs)))))))));
------------------------------------------------------------------------

We replace the symbols with their `@` addresses and feed into our first
compiler to produce an ION assembly program that compiles a primitive lambda
calculus to ION assembly.

I should confess that some of these terms were produced by a program I wrote,
and I have not checked all of them manually. Hopefully, it's plausible this
could be done. Perhaps an acceptable procedure would be to plug terms into
link:../zh23/bubble.html[the animated reducer from my ZuriHac 2023 talk], and
watch closely to ensure each step is valid and the desired result is obatined.
The computer assists, but ultimately human eyes verify.

== Practically ==

We've reached a milestone. Thanks to our previous compiler, never again do we
convert LC to CL by hand.

But there's a catch. For each variable we abstract over, our bracket
abstraction algorithm applies the S combinator to every application. Hence for
N variables, this multiplies the number of applications by 2^N^, which is
intolerable for all but the smallest programs.

Thus our first priority is to optimize bracket abstraction. We stop recursively
adding S combinators as soon as we realize they are unnecessary by modifying
`vCheck` and `unlam`:

------------------------------------------------------------------------
vCheck f = fix (\r t -> t (\x -> False) f (\x y -> r x || r y) undefined);
unlam occurs = fix (\r t -> occurs t
  (t undefined (const (V 'I')) (\x y -> A (A (V 'S') (r x)) (r y)) undefined)
  (A (V 'K') t));
------------------------------------------------------------------------

(I'm unsure if it's worth explaining the optimization as I only understood
after fiddling around with combinators. Here goes anyway: I think of S as
unconditionally passing a variable to both children of an application node.
With a little analysis, we can tell when a child has no need for the variable.)

We desugar these with Y combinators, and inlining the Church-encoded OR.

------------------------------------------------------------------------
\f.Y(\r.\t.t(\x.KI)f(\x.\y.BS(BB)(rx)(ry))?);
\f.Y(\r.\t.ft(t?(K([dV]#I))(\x.\y.[dA]([dA]([dV]#S)(rx))(ry))?)([dA]([dV]#K)t));
------------------------------------------------------------------------

We replace symbols (this time sensibly denoted within square brackets) with
their `@`-addresses and feed it to our previous compiler, which yields massive
but manageable combinatory logic terms.

== Summary ==

Our three compilers are the following:

------------------------------------------------------------------------
`C`TI;``BS`BB;``S``B@!`=##`=#@;``S``B@!`=#;`=#);``R``B`B``BKT``BB`@ `B`:#```BBB;``B`B@ ``R``R:``BBB``BBB;``S``BC``RI``R@%@":;``BC``B`B@ C;``B`RK``R@'B;``R@&``BS``B`C`=#(@(;``B`S``BS`C@#``S``BB``BC``B`BB@)`B@$;`Y``B`B`B@ ``B`BC@*;``RK``B@+``B`C``BB`@ I`B`:#;;`Y``B`S`TK``B`BK``B`BK@,;

B(B(BKT))(BCT);B(C(TK))T;C(BB(B@!(C(BB(B@!(B@ ))))));B@"@ ;B@"(@#(KI));B@"(@#K);B(B(R(BKT)))S;B(BK)(B(BK)(B(BK)T));BK(B(BK)(B(BK)T));B(BK)(B(BK)(B(B(BK))(BCT)));B(BK)(B(BK)(B(BK)(BCT)));B(C(TK))(B(B(RK))(C(BS(BB))@ ));B@+(BT=);@+(BC(S(B(BS(BB))(=#;))(=#))));@"(@#(BB:)(@&(@,##)(@,#@)))(@#:(@+(KK)));C(B@&(C(B@&(S(B@&(B(@$(@,#())(C@%(@,#)))))(B(@"(@$(@,#\)(@#@*@-)))(@$(@,#.)))))(@#@'@.)))(@#@(@-);Y(B(R(@ I))(B(B@&)(B(S(B@"(B(@#T)@/)))(B(@#(C(BBB)(C@))))))));Y(S(B@"(B(@#T)@/))@0);Y(B(R?)(B(C(R:(TI)))(S(BC(B(BB)(B(BB)(B(B(:#`))))))I)));R(B(@)(@(#K))@()(BS(R(@(#I)));BY(B(B(R?))(R(S(BC(B(BB)(B(B@))(B(@)(@(#S))))))I)(BB(BC(C(T(B(@)(@(#K))@')))))));Y(S(BC(B(C(R@((T@')))(S(BC(B(BB)(B@))))I)))(C(BB(B@4(B@3=)))));RK(Y(B(C(RI(@%@1(@,#;))))(BT(C(BB(BB(R(:#;)(BB(B@2@5)))))))));

B(B(BKT))(BCT);B(C(TK))T;C(BB(B@!(C(BB(B@!(B@ ))))));B@"@ ;B@"(@#(KI));B@"(@#K);B(B(R(BKT)))S;B(BK)(B(BK)(B(BK)T));BK(B(BK)(B(BK)T));B(BK)(B(BK)(B(B(BK))(BCT)));B(BK)(B(BK)(B(BK)(BCT)));B(C(TK))(B(B(RK))(C(BS(BB))@ ));B@+(BT=);@+(BC(S(B(BS(BB))(=#;))(=#))));@"(@#(BB:)(@&(@,##)(@,#@)))(@#:(@+(KK)));C(B@&(C(B@&(S(B@&(B(@$(@,#())(C@%(@,#)))))(B(@"(@$(@,#\)(@#@*@-)))(@$(@,#.)))))(@#@'@.)))(@#@(@-);Y(B(R(@ I))(B(B@&)(B(S(B@"(B(@#T)@/)))(B(@#(C(BBB)(C@))))))));Y(S(B@"(B(@#T)@/))@0);Y(B(R?)(B(C(R:(TI)))(S(BC(B(BB)(B(BB)(B(B(:#`))))))I)));\f.Y(\r.\t.t(\x.KI)f(\x.\y.BS(BB)(rx)(ry))?);\f.Y(\r.\t.ft(t?(K(@(#I))(\x.\y.@)(@)(@(#S)(rx))(ry))?)(@)(@(#K)t));Y(S(BC(B(C(R@((T@')))(S(BC(B(BB)(B@))))I)))(C(BB(B@4(B@3=)))));RK(Y(B(C(RI(@%@1(@,#;))))(BT(C(BB(BB(R(:#;)(BB(B@2@5)))))))));
------------------------------------------------------------------------

== Term rewriting; bootstrapping ==

https://arxiv.org/pdf/1812.02243.pdf[Corrado Böhm's PhD thesis (1951)]
discusses self-compilation and presents a high-level language that can compile
itself.

https://tromp.github.io/cl/LC.pdf[John Tromp lists rewrite rules] to further
reduce the size of the output combinatory logic term after bracket abstraction.

Chapter 16 of
https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/[_The
Implementation of Functional Programming Languages_ by Simon Peyton Jones]
gives a comprehensive overview of this strategy.

http://www.cantab.net/users/antoni.diller/brackets/intro.html[Antoni Diller has interactive demos and more references].

https://en.wikipedia.org/wiki/Chicken_or_the_egg[Ancient philosophers thought
about bootstrapping compilers] but their progress was paltry. Or poultry, one
might say.

https://www.joachim-breitner.de/blog/748-Thoughts_on_bootstrapping_GHC[Joachim
Breitner frets about the difficulty of bootstrapping GHC].

https://cakeml.org/[CakeML] is a formally verified bootstrappable ML compiler.