Thursday, June 12, 2014

Why I don't like laziness

Some ppl think lazy functional programming is nicer than strict. At first I thought so as well, but now I think strict is nicer. Not for any engineering reasons, but from a purely mathematical point of view.

The reason has to do with equality. I think about the equality operation a lot, it really brings out the important issues in language design. It's become something of a litmus test for me, if some language feature is dragging down the equality operation, then it probably sucks in other ways too. For example, in Haskell you can do this:

data Natural = Zero | Successor Natural deriving Eq
omega :: Natural
omega = Successor omega

So you have this bizarre number "omega" that is not bottom, and you can pattern-match on it to your heart's content. You can compare it for equality with Zero, Successor Zero and so on, and all those comparisons will happily return False. But try to compare omega to itself, and you get an infinite loop!

That's the problem in a nutshell. Since Haskell is lazy, there are no types that support decidable equality at all! So you might as well allow "deriving Eq" for many more types, like Bool -> Bool. Sure, comparing two functions of that type is undecidable, but it's exactly as undecidable as comparing two lazy Bools in the first place :-)

Imagine for a moment that Haskell was strict. Then we would know, truly irrevocably and forever, that the types that allow "deriving Eq" are exactly the types that have an always terminating equality operation, nothing more and nothing less. In a lazy language, "deriving Eq" can't make such a powerful statement and replaces it with something wishy-washy, and that's why I think strict is nicer.

1 comment:

  1. Strict languages still allow recursive definitions like this omega. Here's one in Idris:

    data N = Zero | Suc N

    omega : N
    omega = Suc omega

    Same thing is possible in OCaml, for example.

    ReplyDelete