parse "BS(BB);Y(B(CS)(B(B(C(BB:)))C));" == "``BS`BB;`Y``B`CS``B`B`C``BB:C;"
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:
We assume the input is valid and contains no numbers in parentheses or
square brackets (so it only uses @ to refer to previous terms and # for
integer constants).
In Haskell we could write:
term acc (h:t)
| h == ')' || h == ';' = (acc, t)
| h == '(' = uncurry (app acc) (term "" t)
| otherwise = if h == '#' || h == '@'
then app acc (h:head t:"") (tail t)
else app acc (h:"") t
where app acc s = term (if null acc then s else '`':acc ++ s)
parse "" = ""
parse s = let (p, t) = term "" s in p ++ ';':parse t
To translate to combinatory logic, we first break our code into more digestible pieces:
pair x y f = f x y;
(||) f g x y = f x (g x y);
(++) xs ys = xs ys (\x xt -> x : (xt ++ ys));
ifNull xs a b = xs a (\_ _ -> b);
add r acc p = r (ifNull acc p ('`':(acc ++ p)));
isPre h = h('#'(==)) || h('@'(==));
suffix f h t = isPre h (t undefined (\a b -> pair (a:[]) b)) (pair [] t) (\x y -> f (h:x) y);
atom r h acc t = suffix (add r acc) h t;
sub r acc = uncurry (add r acc) . r "";
closes h = h(';'(==)) || h(')'(==));
if3 h x y z = closes h x (h('('(==)) y z);
switch r a h t = if3 h pair (sub r) (atom r h) a t;
term acc s = s undefined (\h t -> switch term acc h t);
parse s = term "" s (\p t -> ifNull p ";" (p ++ (';':parse t)));
Scott-encoding pairs implies uncurry is the T combinator, and (.) is
an infix operator with the same meaning as the B combinator.
Thus the above becomes:
``BCT; ``BS`BB; `Y``B`CS``B`B`C``BB:C; ``B`R``BKK`BB; ``C``BBB``S``BS@#``B`B`:#`@"; ``S``B@!`T`##=`T`#@=; ``B`S``BC``C``BS``C``BB@%``C`T?``B@ ``C:K`@ K``C``BBB:; ``BC``B`B@&@$; ``S``BC``B`BB``B`BT@$`TK; ``S``B@!`T`#;=`T`#)=; ``S``BC``B`BB``B`BB@)`T`#(=; ``BC``S``BS``B`C``C@*@ @(@'; `Y``B`B`C`T?@+; `Y``B`S`TK``B`BK``B`BK``B`C`@,K``B`C``BB@"`B`:#;;
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.
The following are friendlier names for the combinators I, K, T, C, Y, and K, respectively.
id x = x; const x _ = x; (&) x f = f x; flip f x y = f y x; fix x = x (fix x); Nothing x _ = x;
Our program starts with a few classic definitions. P stands for "pair".
Just x f g = g x; P x y f = f x y; (||) f g x y = f x (g x y); (++) xs ys = xs ys (\x xt -> x : (xt ++ ys));
As combinators, we have:
BKT; BCT; BS(BB); Y(B(CS)(B(B(C(BB:)))C));
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
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:
B(B@ )@!; B(C(TK))T; C(BB(B@%(C(BB(B@%(B@$)))))); B@&@$; B@&(@'(KI)); B@&(@'K); B(B(R@ ))S;
Our syntax tree goes into the following data type:
data Ast = R [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:
R s = \a b c d -> a s; V v = \a b c d -> b v; A x y = \a b c d -> c x y; L x y = \a b c d -> d x y;
which translates to:
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)));
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 = (:) <$> (char '#' <|> char '@') <*> (flip (:) const <$> 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:
B(C(TK))(B(B(RK))(C(BS(BB))@$)); B@/(BT=); @/(BC(S(B@"(T(#;=)))(T(#)=)))); @&(@':(@*(@0##)(@0#@)))(@'(C:K)(@/(KK))); C(B@*(C(B@*(S(B@*(B(@((@0#())(C@)(@0#)))))(B(@&(@((@0#\)(@'@.@1)))(@((@0#.)))))(@'@+@2)))(@'@,@1); Y(B(R(@$I))(B(B@*)(B(S(B@&(B(@'T)@3)))(B(@'(C(BBB)(C@-))))))); Y(S(B@&(B(@'T)@3))@4);
The babs and unlam functions perform simple bracket abstraction, and
show writes the resulting lambda-free Ast in ION assembly.
show t = t id (\v -> v:[])(\x y -> '`':(show x ++ show y)) undefined; unlam v = fix (\r t -> t (\x -> A (V 'K') (R x)) (\x -> x((==)v) (V 'I') (A (V 'K') (V x))) (\x y -> A (A (V 'S') (r x)) (r y)) undefined); babs t = t R V (\x y -> A (babs x) (babs y)) (\x y -> unlam x (babs 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 "" (\p -> p (\x t -> show (babs x) ++ ";" ++ main t)));
These last few functions are:
Y(B(R?)(B(C(C(TI)(C:K)))(B(B(B(:#`)))(S(BC(B(BB)(B@#)))I)))); BY(B(B(R?))(C(BB(BC(B(C(T(B(@-(@,#K))@+)))(C(BS(B(R(@,#I))(BT=)))(B(@-(@,#K))@,)))))(S(BC(B(BB)(B(B@-)(B(@-(@,#S))))))I))); Y(S(BC(B(C(C(T@+)@,))(S(BC(B(BB)(B@-)))I)))(C(BB@7))); Y(B(C(C(@)@5(@0#;))K))(BT(C(BB(B@#(C(B@#(B@6@8))(:#;K)))))));
We feed the combinators into our first compiler to produce an ION assembly program that compiles a primitive lambda calculus to ION assembly.
I should confess that the above combinator terms were produced by a program I wrote, and I have only checked a few of them. Hopefully, it’s plausible all can be verified by hand.
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 adds an application of the S combinator to every application. Hence for N variables, this multiplies the number of applications by 2N, 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 unlam and adding a helper function occurs:
occurs v t = t (\x -> False) (\x -> x(v(==))) (\x y -> occurs v x || occurs v y) undefined; unlam v t = occurs v t (t undefined (const (V 'I')) (\x y -> A (A (V 'S') (unlam v x)) (unlam v y)) undefined) (A (V 'K') t);
(I’m unsure if it’s worth explaining the optimization in words 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 rewrite these with one-character variable names and Y combinators, and
use @-indexing to refer to other definitions:
Y\a.\b.\c.c(\d.KI)(\d.d(b=))(\d.\e.@"(abd)(abe))?; Y\a.\b.\c.@7bc(c?(K(@,#I))(\d.\e.@-(@-(@,#S)(abd))(abe))?)(@-(@,#K)c);
Our previous compiler turns these into massive but manageable combinatory logic terms.
Summary
Our three compilers are the following:
``BCT;``BS`BB;`Y``B`CS``B`B`C``BB:C;``B`R``BKK`BB;``C``BBB``S``BS@#``B`B`:#`@";``S``B@!`T`##=`T`#@=;``B`S``BC``C``BS``C``BB@%``C`T?``B@ ``C:K`@ K``C``BBB:;``BC``B`B@&@$;``S``BC``B`BB``B`BT@$`TK;``S``B@!`T`#;=`T`#)=;``S``BC``B`BB``B`BB@)`T`#(=;``BC``S``BS``B`C``C@*@ @(@';`Y``B`B`C`T?@+;`Y``B`S`TK``B`BK``B`BK``B`C`@,K``B`C``BB@"`B`:#;; BKT;BCT;BS(BB);Y(B(CS)(B(B(C(BB:)))C));B(B@ )@!;B(C(TK))T;C(BB(B@%(C(BB(B@%(B@$))))));B@&@$;B@&(@'(KI));B@&(@'K);B(B(R@ ))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@"(T(#;=)))(T(#)=))));@&(@':(@*(@0##)(@0#@)))(@'(C:K)(@/(KK)));C(B@*(C(B@*(S(B@*(B(@((@0#())(C@)(@0#)))))(B(@&(@((@0#\)(@'@.@1)))(@((@0#.)))))(@'@+@2)))(@'@,@1);Y(B(R(@$I))(B(B@*)(B(S(B@&(B(@'T)@3)))(B(@'(C(BBB)(C@-)))))));Y(S(B@&(B(@'T)@3))@4);Y(B(R?)(B(C(C(TI)(C:K)))(B(B(B(:#`)))(S(BC(B(BB)(B@#)))I))));BY(B(B(R?))(C(BB(BC(B(C(T(B(@-(@,#K))@+)))(C(BS(B(R(@,#I))(BT=)))(B(@-(@,#K))@,)))))(S(BC(B(BB)(B(B@-)(B(@-(@,#S))))))I)));Y(S(BC(B(C(C(T@+)@,))(S(BC(B(BB)(B@-)))I)))(C(BB@7)));Y(B(C(C(@)@5(@0#;))K))(BT(C(BB(B@#(C(B@#(B@6@8))(:#;K))))))); BKT;BCT;BS(BB);Y(B(CS)(B(B(C(BB:)))C));B(B@ )@!;B(C(TK))T;C(BB(B@%(C(BB(B@%(B@$))))));B@&@$;B@&(@'(KI));B@&(@'K);B(B(R@ ))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@"(T(#;=)))(T(#)=))));@&(@':(@*(@0##)(@0#@)))(@'(C:K)(@/(KK)));C(B@*(C(B@*(S(B@*(B(@((@0#())(C@)(@0#)))))(B(@&(@((@0#\)(@'@.@1)))(@((@0#.)))))(@'@+@2)))(@'@,@1);Y(B(R(@$I))(B(B@*)(B(S(B@&(B(@'T)@3)))(B(@'(C(BBB)(C@-)))))));Y(S(B@&(B(@'T)@3))@4);Y(B(R?)(B(C(C(TI)(C:K)))(B(B(B(:#`)))(S(BC(B(BB)(B@#)))I))));Y\a.\b.\c.c(\d.KI)(\d.d(b=))(\d.\e.@"(abd)(abe))?;Y\a.\b.\c.@7bc(c?(K(@,#I))(\d.\e.@-(@-(@,#S)(abd))(abe))?)(@-(@,#K)c);Y(S(BC(B(C(C(T@+)@,))(S(BC(B(BB)(B@-)))I)))(C(BB@8)));Y(B(C(C(@)@5(@0#;))K))(BT(C(BB(B@#(C(B@#(B@6@9))(:#;K)))))));
Term rewriting; bootstrapping
Corrado Bőhm’s PhD thesis (1951) discusses self-compilation and presents a high-level language that can compile itself.
John Tromp lists rewrite rules to further reduce the size of the output combinatory logic term after bracket abstraction.
Chapter 16 of The Implementation of Functional Programming Languages by Simon Peyton Jones gives a comprehensive overview of this strategy.
Ancient philosophers thought about bootstrapping compilers but their progress was paltry. Or poultry, one might say.
CakeML is a formally verified bootstrappable ML compiler.