|
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). |
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.