Wednesday, July 16, 2014

Codata, co-totality, co-complexity

I've been trying to figure out complexity analysis in Haskell for some time, and now I think I finally understand why it's difficult.

As sigfpe described, there are two universes out there. One is about inductive types and always finite data, and the other is about coinductive types and potentially infinite data. Roughly, the list type in ML is a good example of data, and the list type in Haskell is a good example of codata.

The difference between data and codata affects most things you can say about programs. For example, ML has a concept of totality. The length function on lists is total, because lists are guaranteed to be finite. Haskell, on the other hand, has no useful concept of totality, and the length function is partial. But Haskell has a concept of "co-totality" instead, and the zip function on lists is "co-total", meaning that its result can be pattern-matched to arbitrary depth if the arguments satisfy the same condition. (The idea of "guarded" or "productive" recursion is related to that.)

So if the universe and co-universe are duals, there must be a natural concept of "co-complexity", right? Well, yeah. In a genuinely "co-universe" language, it would be easy to reason about time and space complexity, just like in ML and other languages from the "data universe". But it turns out that Haskell is not quite a "co-universe" language!

Giving away the punchline, data and codata don't correspond naturally to eager and lazy evaluation, as you might have guessed. Instead, data and codata correspond to call-by-value and call-by name! There's a big difference between call-by-name and lazy evaluation (call-by-need), namely that the former will evaluate the same expression several times if needed, while the latter uses memoization and graph reduction all over the place.

If Haskell was a pure call-by-name language, we'd be able to define "co-complexity" for individual functions, in terms of how hard it is to evaluate their result to a given depth. This way, complexity analysis would work compositionally, as you'd expect. But with lazy evaluation, accessing the head of a list becomes cheaper the second time you do it. This way, referential transparency of costs is lost.

Of course, programming in a pure call-by-name language would most likely be unpleasant, and there are good reasons for lazy evaluation to exist. But it was interesting for me to realize that Haskell is not the "co-universe" twin of a strict language like ML, but rather some sort of hybrid, which is harder to reason about than either of the two "pure" approaches.

In summary, it's not codata that makes it hard to reason about complexity, it's the pervasive memoization.