Operational Semantics of Eager Combinator Rewriting

I EXPANDED ON THIS POST AND ADDED IT TO THE MAIN WEBSITE.

I got a question about the operational semantics of the eager combinator rewrite system I use. It's embarrassingly facile and trivial to explain with two pictures, so here goes.

Say, you have a term language where you want to rewrite an expression consisting of combinators. In Egel's case, each combinator knows how to rewrite itself, therefore, corresponds to a procedure or some code.

You could use a stack and push stackframes for F, G, and H. However, I wanted to experiment with another model, rewriting. Note that since we're rewriting eagerly we're rewriting the outermost expression first.

The operational semantics Egel uses is extremely simplistic: Start with the node which is to be rewritten first, store the result where necessary, and continue with the next node to rewrite.

That's it. Note that the resulting graph is still a directed acyclic graph. That's what enables me to implement Egel's interpreter with native C++ reference counted pointers.

This is, of course, a slow and restrictive manner of evaluation. For one, stack based evaluators are simply faster because pushing data to, or popping from, a stack is less computationally expensive than allocating, and deallocating, heap nodes. Second, it's a term rewrite system so you can't allow for assignment since that would usually allow you to create cyclic structures.

The benefits of this model are threefold. For one, you don't run out of stack space which is really important in a functional language as I have experienced, unfortunately. Second, it is still a tree rewrite system so you don't need to care about tail call optimization. Third, you can reference count.

I simply like this model of evaluation, there isn't much more to it.

Notes: Yes, these are thunks or heap allocated stack frames. No, this isn't done with CPS since CPS is a transformation, not an evaluation strategy. Bytecode is generated directly for this model.

More: Egel also supports exceptions which is a natural extension of this model. It is left as an exercise to the reader.

Log 071917

I took a break after running into a few snags. For one, the Ocaml input/output (IO) specification wasn't very good. It neatly describes channels and cleanly separates them into input and output; that looks nice at first glance but what if you want both? I.e., a naive database application usually consists of seek operations followed by reads and writes. It's an odd design decision.

Then there is C++'s manner of working with stdin, stdout and stderr as well as istreams, ostreams and fstreams. They made the standard IO streams uncopyable! Implying you can only pass references but never copy them. Of course, you might be tempted to pass pointers but you run into another whole set of problems. For one, expect lots of template type errors, and also, you're not supposed to call delete when a standard stream goes out of scope.

Then there is the class inheritance design of C++'s streams. It's over-engineered to meet the requirements of an OO type system; here you also see that the type system forces a solution which is simply not that neat though multiple inheritance helps.

Looking at both specifications I can only conclude that C's POSIX file handles specification simply wasn't that bad.

I also started looking at libuv as the basis of file IO, and later multithreading. And I hit another snag: Callbacks don't neatly fit into a mostly referential transparant system. (Well, so far. Unless I come up with a scheme to make it fit.) The problem: Sure you can define a callback, sure it will read values from a pipe, but it can't do anything with it. It simply cannot inform another thread easily to continue evaluation with a calculated value. (Imagine multiple reading threads and one thread who consumes and writes the result back. It's difficult to combine results from multiple threads with one callback.)

I am tempted to roll out my own temporary solution for primitive IO. I am also tempted to ignore libuv and write a PAR combinator using C++ primitives. But libuv is cross-platform, well-maintained, scalable, and popular...

Opaque Combinators

It's design time! As the implementation progresses I am working towards a solution for primitive input/output (IO) in Egel. As a design specification, I simply copied the, or one, interface of Ocaml's primitive IO libraries from a website. Keeping fingers crossed they thought that design through.

That means I am leaving purity behind. But then, if you want pure combinators, you can always build them upon the impure interface so not much is lost.

The bigger problem is that I now need to come up with some kind of scheme for impure 'stateful' combinators. I.e., a fix for file handles, raw pointers, matrices, etc.

So what have I got? For one, the symbol attached to a combinator isn't enough to uniquely describe it. Moreover, equality is problematic and needs to be handled elsewhere. The runtime can't look into the combinator since it simply doesn't know, cannot know, what it contains; but it needs a symbol attached it seems.

Right. A bit foggy but some solution is dawning on me.

Log 071617

Right. I managed to implement the N-Queens problem which the interpreter solves in around 13 seconds, GHC just promptly delivers the solutions.

That either implies I have a very slow runtime -which I know- or GHC sneakily also enjoys the benefit of lazy evaluation on this problem. I.e., I don't understand the solution I translated but the standard functional approach is to generate all board positions and filter out all admissible ones. GHC might benefit from lazy evaluation in that it doesn't need to produce all board positions but just needs to inspect whether a partly constructed solution is admissible according to the constraints, that would give almost back-tracking behavior on the solution space. (If I got it correct, the solution space is over-constrained, you only need 92 out of roughly forty thousand solutions. It helps a lot if you can swiftly dispose of most of them.)

Anyway, this task is far too complex for where the Egel interpreter is now in its development. I decided to implement the solution to a far more trivial problem, Euler project's task one. Sum all the integers from one to a thousand which are dividable by either three or five. Below the code, without the prelude primitives.

namespace ThreeOrFive (

    using System
    using List

    def sum = foldr (+) 0

    def three_or_five = [X -> or ((X%3) == 0) ((X%5) == 0) ]

    def euler1 =
        [ N -> (sum @ (filter three_or_five)) (fromto 1 N) ]

)

using ThreeOrFive

def main = euler1 1000

N-Queens

Woot! The N-Queens problem as translated from Haskell to Egel. I have absolutely no idea what the code does.

namespace System (

    def flip = [ F, X, Y -> F Y X ]

    def or =
        [ false, false -> false
        | X, Y         -> true ]

    def and =
        [ true, true    -> true
        | X, Y          -> false ]

    def @ =
        [ F, G, X -> F (G X) ]

)

namespace List (

    using System

    def length =
        [ nil -> 0
        | cons X XX -> 1 + (length XX) ]

    def foldl =
        [ F, Z, nil -> Z
        | F, Z, cons X XX -> foldl F (F Z X) XX ]

    def foldr =
        [ F, Z, nil -> Z
        | F, Z, cons X XX -> F X (foldr F Z XX) ]

    def ++ =
        [ nil, YY -> YY
        | cons X XX, YY -> cons X (XX ++ YY) ]

    def map =
        [ F, nil -> nil
        | F, cons X XX -> cons (F X) (map F XX) ]

    def reverse = 
       foldl (flip cons) nil

    def block =
        [ 0 -> nil
        | N -> cons (N-1) (block (N-1)) ]

    def fromto =
        [ X, Y -> 
            if X < Y then
                reverse (map [ N -> N + X ] (block (Y-X)))
            else nil ]

    def zipwith =
        [ Z, cons X XX, cons Y YY -> cons (Z X Y) (zipwith Z XX YY)
        | Z, XX, YY               -> nil ]

    def any =
        [ P, nil        -> false
        | P, cons B BB  -> if P B then true else any P BB ]

    def all =
        [ P, nil        -> true
        | P, cons B BB  -> if P B then all P BB else false ]

    def elem =
        [ X -> any ((==) X) ]

    def notelem =
        [ X -> all ((!=) X) ]

    def insertEverywhere =
        [ X, nil -> {{X}}
        | X, cons Y YY -> cons (cons X (cons Y YY))

                 (map (cons Y) (insertEverywhere X YY)) ]

    def concatMap =
        [ F -> foldr ((++) @ F) nil ]

    def permutations =
        foldr (concatMap @ insertEverywhere) {{}}
)

namespace NQueens (

    using System
    using List

    def nqueens =
        [ 0, NCOLS     -> cons nil nil
        | NROWS, NCOLS ->
            foldr
              [ SOLUTION, A ->
                  A ++
                  (foldr
                    [ICOL, B ->
                        if safe (NROWS - 1) ICOL SOLUTION
                          then B ++ ({SOLUTION ++ {ICOL}})
                          else B]
                    nil
                    (fromto 1 (NCOLS+1))) ]
            nil
            (nqueens (NROWS - 1) NCOLS) ]

    def safe =
        [ IROW, ICOL, SOLUTION ->
            notelem true
             (zipwith
                [SC, SR ->
                   or (ICOL == SC) 
                  (or (SC + SR == ICOL + IROW) 
                      (SC - SR == ICOL - IROW))]
                SOLUTION
                (fromto 0 IROW)) ]
)

using List
using NQueens

def main = length (nqueens 8 8)

Unfortunately, it takes some.. time.. A lot longer than Haskell which just prompty gives the answer.

[marco@stallion src]$ time ./egel ../examples/nqueens.eg 
92

real 0m13.020s
user 0m13.000s
sys 0m0.001s

But then again, I am more looking for automating tasks on matrix operations then anything else. So, I am happy.

Log 071417

Over the last few days, I fixed a number of trivialities and added some basic functionality. Escaping/unescaping on characters and strings, got an interactive prompt running, added basic -recursive- comparison operators on runtime objects, fixed a lifting bug in try/catch (and introduced a new one), and some more stuff.

I am working towards implementing an N-queens example in Egel but hit a snag, a core dump on a program. Well, that's a long time ago. So, a) good I started on a less trivial program, and b) bad I hit a core dump on that. That shouldn't happen anymore.

A well. Just wrinkling out stuff, I guess. Hope this bug ain't too pesky.

EDIT: Didn't turn out too pesky. I forgot a recursive case in desugaring lists, which probably implied code generation on an AST node which shouldn't exist. Phew...

Log 071317

Right. So the way I work is that I program a bit, hit a problem, ponder too long on the problem, lose interest, and half a year later -after I forgot what that nasty little thing was all about- return to coding.

Ridiculous, I admit.

Anyway, I moved twenty lines around and went onto the next problem of getting interactive mode right.