4 ms·
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 theoretical
by grapevines 12y ago
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 https://github.com/jbodeen/-ava
- asQuirreL 12y agoThis 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 http://en.wikipedia.org/wiki/SECD_machine [2]: http://en.wikipedia.org/wiki/SKI_combinator_calculus http://en.wikipedia.org/wiki/SKI_combinator_calculus [3]: http://en.wikipedia.org/wiki/B,C,K,W_system http://en.wikipedia.org/wiki/B,C,K,W_system [Turner79]: http://courses.cecs.anu.edu.au/courses/COMP3610/assignments/Asst1/Turner-Combinators.pdf http://courses.cecs.anu.edu.au/courses/COMP3610/assignments/... (apologies, I couldn't seem to find a version with an intact abstract).
- polymatter 12y agoInteresting 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 12y agoYou're right `h :: a -> c`.