3 ms·

I've slowly come to the opinion that laziness is not the best idea, even from a pure mathematical point of view. There are large mathematical benefits to using

I've slowly come to the opinion that laziness is not the best idea, even from a pure mathematical point of view. There are large mathematical benefits to using a strict language like SML. One important benefit to me is that strictness allows you to have an equality operation with a very strong mathematical guarantee, namely that the types for which equality can be automatically defined are precisely the types for which equality is decidable (always terminates). A lazy language throws that out the window. In a strict language you can define both a type of guaranteed-finite lists with decidable equality and a type of potentially-infinite streams, while in a lazy language you only have the latter. I wrote about it in more detail here: http://slepnev.blogspot.ch/2014/06/is-laziness-wrong-for-equality.html http://slepnev.blogspot.ch/2014/06/is-laziness-wrong-for-equ...

wyager 12y ago
But mathematics is non-strict. One can define functions that terminate when evaluated lazily but don't terminate when evaluated strictly. These kinds of functions are prevalent in mathematics.
- cousin_it 12y ago
  Does your belief that "mathematics is non-strict" go as far as saying that the type of natural numbers: data Natural = Zero | Successor Natural must include this member as well: omega :: Natural omega = Successor omega bool1 = (omega == Zero) -- returns False bool2 = (omega == Successor Zero) -- returns False bool3 = (omega == omega) -- whoops, infinite loop The moral is that some parts of mathematics may be lazy, but mathematical induction has gotta be strict. Since many functional programs rely on induction for proofs of termination, correctness and resource usage, that means they should be strict as well.
  - wyager 12y ago
    >Since many functional programs rely on induction for proofs of termination, correctness and resource usage, that means they should be strict as well. Am I incorrect in thinking that any strict program proven to be correct and terminating is also correct as a lazy program?
    - cousin_it 12y ago
      Yeah, that's true for programs, i.e. things that accept no arguments. Lazy evaluation provably makes more programs terminate than any other evaluation strategy. But it's kind of misleading for functions that accept arguments, like numbers or lists. Most functions in a lazy language can fail to terminate, because the arguments could fail to terminate or could be non-standard entities like omega. So, for example, the statement "computing the length of a list always terminates" is true in a strict language but not in a lazy one. In general, strict languages allow you to say more about termination and time/space complexity of functions than lazy languages. For example, the statement "computing the length of a list takes O(1) space" is true in a strict language, but in a lazy language it's difficult to say what the statement even means, and in most practical cases it's false. Computing length with either foldr and foldl uses at least O(n) space, and the usual advice is to use foldl', which has a strictness annotation. I think this should be alarming to anyone who recommends lazy evaluation as the right default. In slightly more complicated cases, like sorting a list, there's no sensible way to assign a time or space complexity at all, because it depends on how the function is called and how much of the result is used by the caller. People sometimes claim that's an advantage of lazy languages, e.g. implementing quickselect in terms of quicksort and claiming that quickselect will only evaluate as much of quicksort as needed. I think that's a hack. We need to be able to reason about the time and space complexity of a program in terms of its parts, without relying on implementation details of the parts.

wyager 12y ago

But mathematics is non-strict. One can define functions that terminate when evaluated lazily but don't terminate when evaluated strictly. These kinds of functions are prevalent in mathematics.

cousin_it 12y ago
Does your belief that "mathematics is non-strict" go as far as saying that the type of natural numbers: data Natural = Zero | Successor Natural must include this member as well: omega :: Natural omega = Successor omega bool1 = (omega == Zero) -- returns False bool2 = (omega == Successor Zero) -- returns False bool3 = (omega == omega) -- whoops, infinite loop The moral is that some parts of mathematics may be lazy, but mathematical induction has gotta be strict. Since many functional programs rely on induction for proofs of termination, correctness and resource usage, that means they should be strict as well.
- wyager 12y ago
  >Since many functional programs rely on induction for proofs of termination, correctness and resource usage, that means they should be strict as well. Am I incorrect in thinking that any strict program proven to be correct and terminating is also correct as a lazy program?
  - cousin_it 12y ago
    Yeah, that's true for programs, i.e. things that accept no arguments. Lazy evaluation provably makes more programs terminate than any other evaluation strategy. But it's kind of misleading for functions that accept arguments, like numbers or lists. Most functions in a lazy language can fail to terminate, because the arguments could fail to terminate or could be non-standard entities like omega. So, for example, the statement "computing the length of a list always terminates" is true in a strict language but not in a lazy one. In general, strict languages allow you to say more about termination and time/space complexity of functions than lazy languages. For example, the statement "computing the length of a list takes O(1) space" is true in a strict language, but in a lazy language it's difficult to say what the statement even means, and in most practical cases it's false. Computing length with either foldr and foldl uses at least O(n) space, and the usual advice is to use foldl', which has a strictness annotation. I think this should be alarming to anyone who recommends lazy evaluation as the right default. In slightly more complicated cases, like sorting a list, there's no sensible way to assign a time or space complexity at all, because it depends on how the function is called and how much of the result is used by the caller. People sometimes claim that's an advantage of lazy languages, e.g. implementing quickselect in terms of quicksort and claiming that quickselect will only evaluate as much of quicksort as needed. I think that's a hack. We need to be able to reason about the time and space complexity of a program in terms of its parts, without relying on implementation details of the parts.