6 ms·

True! I think pattern matching and the high-powered static type system really pull a lot of weight here, though. Haskell's types are a whole other dimension of

by Twisol 4y ago

True! I think pattern matching and the high-powered static type system really pull a lot of weight here, though. Haskell's types are a whole other dimension of domain modeling. You can encode algebraic data types as pure lambdas, but it's much less pleasant IMHO. (Laziness also bakes some common streaming patterns into the language core, which I find really nice, but it also makes it harder to totally understand what's going on sometimes, so it's a bit more of a toss-up.) Point being, nobody wants to model their data structures as pure lambdas; even primitive integers are an addition on top of the lambda calculus. > For an example of a non-trivial program I don't think I'm taking the point you wanted me to from this program. It's under 30 lines, yet I'd need to pore over this for twice as many minutes to comprehend what it's doing. I can see the lambda abstractions and applications clear as day, but what they're doing I couldn't say. (The comments clearly say it's a universal binary LC interpreter, but we don't usually judge languages by their comments.) EDIT: Right, okay, it's a submission to the the International Obfuscated C Code Contest. If it's obfuscated, then indeed, I'm not meant to comprehend it easily. Not sure that sells the lambda calculus.

ackfoobar 4y ago
> pure lambdas Also, in lambda calcalus there is no recursion built-in. You have to build it yourself with the Y combinator.
- tromp 4y ago
  Right; you just add definitions you need like let Y = \f. (\x. x x) (\x. f (x x)) in program-using-Y which is the slightly more legible version of (\Y. program-using-Y) (\f. (\x. x x) (\x. f (x x))
jart 4y ago
Spoiler alert, but if you want a tutorial on understanding Tromp's calculus, then here's the readable version of his IOCCC entry with cryptograms and everything deciphered. https://justine.lol/lambda/ https://justine.lol/lambda/
tromp 4y ago
> You can encode algebraic data types as pure lambdas, but it's much less pleasant IMHO Not that much less, since you can manually translate back your Haskell code to lambda calculus. E.g. your List a = Nil | Cons a (List a) rewrites to let Nil = \n\c. n Cons = \x\y. \n\c. c x y in ... Of course the type system is what helps you write correct Haskell code in the first place, so the untyped lambda calculus will be painful for debugging wrongly typed code.

by Twisol 4y ago

ackfoobar 4y ago

> pure lambdas Also, in lambda calcalus there is no recursion built-in. You have to build it yourself with the Y combinator.

tromp 4y ago
Right; you just add definitions you need like let Y = \f. (\x. x x) (\x. f (x x)) in program-using-Y which is the slightly more legible version of (\Y. program-using-Y) (\f. (\x. x x) (\x. f (x x))

jart 4y ago

Spoiler alert, but if you want a tutorial on understanding Tromp's calculus, then here's the readable version of his IOCCC entry with cryptograms and everything deciphered. https://justine.lol/lambda/ https://justine.lol/lambda/

tromp 4y ago

> You can encode algebraic data types as pure lambdas, but it's much less pleasant IMHO Not that much less, since you can manually translate back your Haskell code to lambda calculus. E.g. your List a = Nil | Cons a (List a) rewrites to let Nil = \n\c. n Cons = \x\y. \n\c. c x y in ... Of course the type system is what helps you write correct Haskell code in the first place, so the untyped lambda calculus will be painful for debugging wrongly typed code.