> Oh great, this would only add hundreds of lexemes to your average Haskell file! I'd rather only use laziness when it's absolutely necessary. > Reference mut

> Oh great, this would only add hundreds of lexemes to your average Haskell file! I'd rather only use laziness when it's absolutely necessary. > Reference mutation is a single implementation of lazy semantics. The only way you can avoid mutation in an implementation of laziness is to use a key-value container that maps thunk IDs to their respective contents. This imposes an extra cost, logarithmic in the number of thunks in your computation. I don't think you'd like this implementation. I'm aware that my implementation has deficiencies, e.g., it isn't thread-safe, and it doesn't support polymorphic lazy values. And, of course, because the compiler isn't aware of what I'm doing, I don't get benefits that Haskellers take for granted, like stream fusion and whatnot. But my implementation does capture the essence of laziness: computing an expression when you first need its result, and memoizing this result to avoid recomputing it again. > You say that as if it's a good thing. If I wanted to deal with every detail of the evaluation model, I'd program in assembly. I don't think you can meaningfully abstract the evaluation strategy in a general-purpose programming language. Note that having the Church-Rosser property isn't enough: It says absolutely nothing about the impact of picking this or that reduction strategy on the cost of a computation. Programmers care about that too. > Nor does it in your example. (...) let's not pretend that your example demonstrates that. It does. The types `foo` and `foo lazy` are very different, and ML's type checker will let you know if you wrongly conflate them. > pretending you don't have unsafe stateful mutation in languages like ML. Using reference cells in ML is perfectly safe as long as your program is single-threaded. It's unsafe in a multi-threaded context, but the same is true of Haskell's `IORef`. And I don't pretend that there's no mutation in ML. I'm perfectly aware that ML isn't a pure language, and every expression is potentially effectful unless proven otherwise. Just like every Haskell expression is potentially nonproductive unless proven otherwise. > You didn't actually say that in either of those comments. I did. Call-by-push-value distinguishes between value types (sums, tensor products) and computation types (categorical products, functions), which live in two different categories, related by a pair of adjoint functors. The composition of these adjoint functors is precisely the usual monad for whatever kind of effects your computations might have. (Corollary: if your computations are pure, the adjunction is actually an equivalence of categories. It becomes patently clear that nontermination is an effect!) All of this is explained in the papers ( http://www.cs.bham.ac.uk/~pbl/papers/ http://www.cs.bham.ac.uk/~pbl/papers/ ), so I didn't feel a need to repeat it here. > You're the one advocating for the compiler telling you when your program is divergent. When did I say that? What I actually said is “using a strict language prevents computational effects from infecting values”. Laziness pushes nontermination far away from its source, just like dynamic typing pushes type errors far away from their source. Of course, both laziness and dynamic typing have their place - it just isn't “everywhere in the program”.