Simon Peyton Jones
π€ SpeakerAppearances Over Time
Podcast Appearances
It's a very simple translation.
You can give the whole translation in half a dozen lines.
But then you have this mess of S's and K's.
And S and K reduction is very, very easy.
So it's like the machine code of functional programming.
That's one way to think of it.
There are three combinators, SK and I. And they have simple reduction rules.
Here they are.
I of X equals X. KXY equals X. SXYZ is X of Z applied to Y of Z. End of story.
That's all.
So very simple, right?
So now all I've got to do is take my lambda, translate it into a giant tree of SK accommodators, right?
S applied to K, applied to I of three, and S of Z of, just a huge tree of S's and K's, right?
Now simply apply the rewrite rules I gave you, and that is program execution.
It's rather astonishing that that can execute arbitrarily complicated programs, but it can.
Don't you think that's rather amazing?
Now, then I can take an arbitrary Haskell program, I can translate it into lambda terms, and I can translate those lambda terms into SMK, very simple transformation, and I can just run those three rules, and it'll produce the output of the Haskell program.
That's pretty amazing.
And indeed, there is an implementation of Haskell that uses exactly this.
It's called MicroHS, and my colleague Leonard Augustin has built it.