Comment by joseda-hg
3 days ago
It's too basic for what you need but the video from eyesomorphic [1], is a wonderful conceptual introduction
3 days ago
It's too basic for what you need but the video from eyesomorphic [1], is a wonderful conceptual introduction
> Whilst it certainly isn't a contender for modern programming languages
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.
[1] https://www.ioccc.org/2019/lynn/index.html
> 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].
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.
I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness).
1 reply →
For anyone who's interested - Ben Lynn also has a series of articles that explain the creation of that compiler and add further enhancements:
https://crypto.stanford.edu/~blynn/compiler/
video author is using 3b1b's manim (https://github.com/3b1b/manim). wonderful presentation.