Since the other examples have Haskell equivalents, I believe the variable duplicating combinator is `join` in Haskell, but I'm not near ghci to test.
I go back and forth on how useful these sorts of combinators are. I do appreciate how they at least have to be explicitly declared in Haskell, as opposed to verb trains in J. But I've still gotten complaints from teammates about what the fuck `liftM2 . liftM2` is supposed to mean.
Note for anyone else who missed it, there are expression evaluators embedded in this post. You have to click inside the evaluator and press return (and can edit, etc). Look for the "λ>"
I did as well, and actually came here to see if anyone else had commented on that.
WKx
=> Kxx
=> x
CKCx
=> KxC
=> x
After the first application they both end up in essentially the same state (the `C` in the second case is going to be discarded so it really doesn't matter what's there).
> Basically I preferred solutions that avoided W, since you're then working in a subset of the language that is definitely terminating and affine.
Ah, that makes a lot of sense. I mostly just thought my version was the obvious one - my first thought of how to do nothing was to duplicate something and then drop one of the dupes. I have very little grounding in lambda calculus, though, and generally find the other combinators harder to reason about.
There are tricky aspects, and I've tripped up a few times over the years. Most annoying is trying to make a 'step' function from lambda terms to lambda terms; we either need to produce a separate closure type instead, or encode those closures to lambda terms (which may defeat the point of "reducing"), or perform explicit substitution a la call-by-name (duplicating work). I don't think I've ever got all the details of capture-avoiding substitution right (I get part way there, then just copy/paste someone else's code ;) ).
I'm a big fan of combinatory logic. The rabbit hole goes really deep, with connections to quantum computing (via the linear combinators mentioned in the article), philosophy (e.g. John Tromp's investigation of Kolmogorov Complexity using binary combinatory logic and lambda calculus), and also to type theory and fundamental mathematics (e.g. illative combinatory logic, which I've played with on my blog http://chriswarbo.net/blog/2012-12-01-typed_combinators.html ).
My ioccc winner was a compiler from lambda calculus to SK combinators, written in SK combinators (well, written in the lambda calculus and compiled using a Haskell program) http://ioccc.org/years.html#1998_fanf
Lennart Augustsson won the IOCCC a couple of times by basically writing a program in Lazy ML and hand-compiling it to C using the usual graph reduction techniques http://ioccc.org/winners.html#A I think using supercombinators rather than SK style.
I found the book "An Introduction to Lambda Calculi for Computer Scientists"[1] to be a good intro to these concepts. For those who want to go further, books by Henk Barendregt[2] are widely considered to be a reference to lambda-calculus and combinators.
I'm really curious why there haven't been hardware improvements that focus on evaluating combinatory logic. It seems like a great idea, especially since parallelization is a lot easier.
16 comments
[ 2.6 ms ] story [ 41.7 ms ] threadI go back and forth on how useful these sorts of combinators are. I do appreciate how they at least have to be explicitly declared in Haskell, as opposed to verb trains in J. But I've still gotten complaints from teammates about what the fuck `liftM2 . liftM2` is supposed to mean.
Of course they're not really useful for programming; they're more interesting as a compilation target, formal reasoning, and some fun puzzles.
(although in this case I just didn't find I = WK)
I should actually add a note about that, since a few people have pointed it out.
Ah, that makes a lot of sense. I mostly just thought my version was the obvious one - my first thought of how to do nothing was to duplicate something and then drop one of the dupes. I have very little grounding in lambda calculus, though, and generally find the other combinators harder to reason about.
Lambda calculus allows for a surprisingly simple self-interpreter [1]. Here is one, written with De Bruijn indices:
(λ 1 1)(λ λ λ 1(λ λ λ λ 3(λ 5(3(λ 2(3(λ λ 3(λ 1 2 3)))(4(λ 4(λ 3 1(2 1)))))) (1(2(λ 1 2))(λ 4(λ 4(λ 2(1 4)))5))))(3 3)2)(λ 1((λ 1 1)(λ 1 1)))
This includes a tokenizer/parser of (binary encoded) lambda calculus terms.
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html
Of course, de Bruijn indices can help with this, and I'm a big fan. They get a lot of hate though, e.g. there seems to be an entire CS sub-discipline dedicated to ever-more-elaborate ways to avoid/hide de Bruijn indices ;) (e.g. https://en.wikipedia.org/wiki/Higher-order_abstract_syntax https://arxiv.org/pdf/1807.04085.pdf https://arxiv.org/pdf/1111.0085.pdf http://lambda-the-ultimate.org/node/544 etc.)
Lennart Augustsson won the IOCCC a couple of times by basically writing a program in Lazy ML and hand-compiling it to C using the usual graph reduction techniques http://ioccc.org/winners.html#A I think using supercombinators rather than SK style.
This book is where I learned this stuff: https://www.microsoft.com/en-us/research/publication/the-imp...
Fresh out of college I was really into lambda calculus and combinators, and wrote a pretty similar blog post to this article, maybe just a bit simpler: https://log.kv.io/post/2008/03/02/ski-calculus-in-haskell-sh...
[1] https://www.amazon.com/dp/0954300653
[2] "The Lambda Calculus — Its Syntax and Semantics" and "Lambda Calculus with Types"