Hacker News new | ask | show | jobs
by bjourne 2498 days ago
Afaik, Haskell is a realization of the (typed!) lambda calculus. Lisps aren't because they don't do lazy evaluation. The LC beta reduction of (\a. a) (\c. d) (\e. f) is (\c. d) (\e. f) but most lisps will reduce it to (\a. a) d. This might seem like a minor detail but means general recursion using the y combinator isn't actually implementable in lisps (I could be wrong though).
3 comments

> Afaik, Haskell is a realization of the (typed!) lambda calculus. Lisps aren't because they don't do lazy evaluation.

Lazy evaluation is just one possible operational semantics for a lambda calculus. Eager evaluation is another. In fact, all of the versions of lambda calculi presented in Benjamin Pierce's widely-read textbook "Types and Programming Languages" feature eager evaluation rather than lazy evaluation.

So the claim that the reason that Lisps aren't based on the lambda calculus is due to lack of lazy evaluation is incorrect. There are other reasons that Lisps diverge from lambda calculi but the evaluation strategy isn't one of them.

> general recursion using the y combinator isn't actually implementable in lisps

I think the 'typed' bit is key. You can't implement Y in plain old Haskell because it would need to recurse infinitely during type-checking.

It's valid Haskell 98 with a type constructor: http://r6.ca/blog/20060919T084800Z.html. But in GHC I think the first code snippet without NOINLINE still crashes, it's a perma-bug: https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...

Some type systems do support equi-recursive types without the type constructor, e.g. Whiley (http://whiley.org/2013/04/21/iso-recursive-versus-equi-recur...). Maybe there you could implement Y without a type signature and have the recursive type inferred.

The main problem is speed. Using the Y combinator is going to mess up whatever code flow analysis the compiler has, unless it's using some cutting edge optimization research that I haven't been able to find.

There is a strongly-typed definition of Y here:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

Some enterprising hacker should research who should be credited for the strongly-typed recursive def of Y.
x y z means (x y) z by definition, so there's only one way to reduce that expression.