[grapevines]

This is similar to an idea that I've been kicking around.

It is basically a arbitrary precision beta-reducer for untyped lambda calculus. I think I theoretically would need a machine that only needs four instructions on a theoretical machine (presumably some sort of FPGA), those being write, load, flip, and meld.

I bring this up, because instead of compiling to C, you could simply use a general purpose beta-reducer, and this would allow for arbitrary precision computation instead of being limited to 32 bits or 64 bits or whatever.

It is written in Agda, meaning that it could be a compiler for any arbitrary calculus that could be translated into an untyped lambda calculus.

Unfortunately, my adviser told me that it is a side-project due to lack of theoretical grounding.

You can check it out here: https://github.com/jbodeen/-ava

[asQuirreL]

This idea has been knocking around the collective consciousness of computer science for a while now. For example, the SECD machine [1], a virtual machine for functional programming languages to target. Then there are also examples of people compiling functional programming languages to various lambda calculus bases, such as SKI [2], and BCKW [3]. Through the judicious use of some extra combinators, you can also get more compact "object code"[Turner79].

One advantage of compiling to something like an SKI or BCKW basis (or a mix) is that you can represent abstraction (functions/closures) without bound variables, or scoping, which can be a pain to implement (esp. in hardware).

Take, for example, the SKI basis. Suppose you had two functions, with types as follows:

  f :: a -> b
  g :: b -> a -> c

And you wished to combine them in the natural way to get `h`:

  h :: b -> c
  h x = g (f x) x 

Then, to achieve the same with S, K and I combinators we do the following (assuming we have SKI representations of `f, g` as `F, G`.

  H := S(S(KG)F)I

The `x` has disappeared! But, if we apply H to some CL expression `X` we get:

  HX = S(S(KG)F)IX
     = S(KG)FX(IX)    ;; apply S
     = KGX(FX)(IX)    ;; apply S   
     = G(FX)(IX)      ;; apply K
     = G(FX)X         ;; apply I

We can use S to Split (duplicate) parameters, and K to Kill (ignore) parameters, in a very straight forward way. Imagine the AST of the original code:

     App
     /\
    /  \
   App  x
   /\
  / App
  g /\
   /  \
   f  x

Every `App` is replaced with an `S`, every `x` with an `I`, everything else (`y`) is replaced with `Ky`. In my example, I have also gone to the trouble of "optimising" `S(KF)I` away, as it is equivalent to just `F`.

Interesting stuff, and plenty of theoretical grounding to boot. Especially as this sort of thing has started enjoying a renaissance, in the likes of "point-free" notation in languages like Haskell.

[1]: http://en.wikipedia.org/wiki/SECD_machine [2]: http://en.wikipedia.org/wiki/SKI_combinator_calculus [3]: http://en.wikipedia.org/wiki/B,C,K,W_system [Turner79]: http://courses.cecs.anu.edu.au/courses/COMP3610/assignments/... (apologies, I couldn't seem to find a version with an intact abstract).

[polymatter]

Interesting stuff.

btw I think the type of your the function h is a -> c. I know its a minor typo, but it confused me while I was trying to follow.

[asQuirreL]

You're right `h :: a -> c`.