310 points by MrBuddyCasino 5 days ago | 48 comments
exikyut 3 days ago
But I can't quite wrap my mind around the core concepts and internalize them into a mental model. It's too different from the simple world of imperative C or scripting languages I guess I call home. So I'm left watching das blinkenlights from the outside, as my attention span chokes on the layers of computer science incorporated into typical explanations. *shrug*
I'd be very interested if anyone knows of an ELI5-style alternate path I could walk to break each of the concepts down one at a time. (I ask because I think this is (currently) the kind of thing I think ChatGPT would struggle to present as effectively as a human.)
kccqzy 3 days ago
Lambda calculus is the same. You can easily define the data structure to represent a program in untyped lambda calculus and then write an interpreter for it. Then go implement some interesting concepts such as the Y combinator or the Omega combinator. If you find lambda calculus too difficult to do things like arithmetic or linked lists, you don't have to stick with Church numerals or Scott encodings. Just introduce regular natural numbers and lists as ground types; when you later have a better understanding, write programs to transform regular numerals from and to Church numerals and bask in the fact that they are isomorphic.
anyfoo 2 days ago
I had the luck of reading that quote while I was an undergrad. I did not actually pursue a career in pure math, but it certainly helps me every time I want to understand some math in order to apply it. (Lambda calculus, type systems, Fourier/Laplace/z-transform, ...)
prakashrj 3 days ago
https://www.youtube.com/watch?v=LXhsutNKhec
Just one programming book was able to help my son, who is 12 yrs old, learn lambda calculus and write a meta circular evaluator.
WorldMaker 3 days ago
joseda-hg 3 days ago
tromp 3 days ago
Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1], or equivalently, into BLC programs.
JadeNB 3 days ago
That's what Turing completeness means, though; you can do the same thing with C, with the same provisos. (Conal Elliott has an amusing satire on this: http://conal.net/blog/posts/the-c-language-is-purely-functio... .) It's not that the lambda calculus isn't sufficiently expressive, just that it's not a language in which humans want to write.
tromp 3 days ago
JadeNB 3 days ago
I was referring to the Turing completeness of the lambda calculus, not of Haskell. But, again, I think that trying to work directly with lambda expressions everywhere, even if it is possible and, as you say, straightforward for "vanilla" Haskell, quickly shows why we put some semantic sugar over it. That is to say, it's certainly true that, in an obvious sense, the layer of semantic sugar is thinner for Haskell than for C, but it's still "just" semantic sugar, and still just as conceptually important, in both cases.
dunham 3 days ago
nakedneuron 3 days ago
JadeNB 3 days ago
jart 3 days ago
troad 2 days ago
One thing I saw you write recently is that chasing the newest fads is a distraction. That makes sense, but if you don't mind me asking, what do you think one should focus on instead? Which are the classic languages, tools, mindsets, and CS concepts that one must master?
jart 2 days ago
I don't remember saying that. You might be thinking about https://justine.lol/ape.html where I said we should be focusing on the old things that matter which aren't going away, like UNIX magic numbers, C libraries, and computer science. But I've got nothing against the new. I think AI for example is exciting. Ultimately you should focus on whatever summons your passion and curiosity. Since if you're tapped into that divine energy within, then you can make anything work, and others will agree. Even if it's just boring old numbers.
Joker_vD 3 days ago
lucasoshiro 3 days ago
https://lucasoshiro.github.io/software-en/2020-06-06-lambdas...
Please note that I'm not an expert in lambda calculus, just a curious nerd and it won't explain everything, like the reductions, combinators and so on. But there I explain how to implement simple types (int, boolean, pairs and lists) using Church encoding, let expressions and recursion using the Y combinator (yay, I finally used the expression "Y combinator" on HN!). Everything that we need to implement a quicksort (which is a relatively complex algorithm) using the almost nothing that we have in lambda calculus.
Another point is that it's all implemented in Python, using the Python notation instead of the lambda calculus notation, so you can run the code in your machine and play with the examples
Joker_vD 3 days ago
tromp 3 days ago
[1] https://www.ioccc.org/2012/tromp/
[2] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d8...
mbivert 3 days ago
(λ (λ 1 (λ 1)) (λ 2 1))
Binary λ-calculus is then merely about finding a way to encode those three things in binary; here's how the author does it (from the blog post): 00 means abstraction (pops in the Krivine machine)
01 means application (push argument continuations)
1...0 means variable (with varint de Bruijn index)
The last one isn't quite clear, but she gives examples in `compile.sh`: s/9/11111111110/g
s/8/1111111110/g
s/7/111111110/g
s/6/11111110/g
s/5/1111110/g
s/4/111110/g
s/3/11110/g
s/2/1110/g
To check your understanding, you may want to try to manually convert some λ-expressions using those encoding rules, starting with simple ones, and check what you have with what `compile.sh` yields.[0]: https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...
jart 3 days ago
mbivert 2 days ago
shayansm1 3 days ago
mason_mpls 3 days ago
memming 5 days ago
johnisgood 3 days ago
In fact, if the VM is Turing complete, it can theoretically emulate any computation, including its full implementation, even from a small subset of operations.
The point is that the 43-byte implementation does not need to encode the entire VM explicitly. For example, if the VM has built-in primitives for looping, branching, and memory management, the minimal implementation can leverage these to rebuild the remaining functionality.
tromp 3 days ago
The 521 byte interpreter on the other hand is written in x86 assembly, a language much less suitable for writing BLC8 interpreters than BLC8 itself.
Btw, with my latest lambda compiler, the BLC8 self interpreter is only 42 bytes:
λ 1 ((λ 1 1) (λ (λ λ λ 1 (λ λ λ 2 (λ λ λ (λ 7 (10 (λ 5 (2 (λ λ 3 (λ 1 2 3)))
(11 (λ 3 (λ 3 1 (2 1))))) 3) (4 (1 (λ 1 5) 3) (10 (λ 2 (λ 2 (1 6))) 6))) 8)
(λ 1 (λ 8 7 (λ 1 6 2)))) (λ 1 (4 3))) (1 1)) (λ λ 2 ((λ 1 1) (λ 1 1))))
[1] https://www.ioccc.org/2012/tromp/Dansvidania 3 days ago
johnisgood 3 days ago
cess11 3 days ago
From TFA. I think it's a very good article.