Comment by KirinDave

7 years ago

Well, occasionally you'll run across stuff like this. Because there is a deep correspondence between functions, types, and logic and Haskell has a rich academic tradition that extends alongside its more pragmatic engineering tradition, you get these curious examples of folks transcribing mathematical or logical ideas into code.

We don't use loeb very often (and it's not the abstraction of choice to build a spreadsheet; a memoized comonad is still quite popular idea there), but moeb (or rather, rewriting it as fix) comes up with recursive uses of functions and can be quite elegant.

In cases like this, you can imagine to recognize perfomance benefits on instances of moeb, and if you can have you optimizer turn other loops into something like moeb then you can optimize a wide, wide range of problems. It's a mistake to think it's "meant" for anything. It's almost a joke of a name, Löb's theorem is about how self-referential systems can't be sound.

It's worth noting though that the story doesn't end there. There is a kind of extraction of `fix` (moeb id) that can be expressed at the level of types (often called Fix). Fix has lots of uses (because recursive types are our bread and butter), but one of the most interesting is called "Recursion Schemes." In recursion schemes, we recognize that by assuming certain specific properties of a data structure (usually, that it is a functor), we can generalize it and then use that generalization to write functions to recurse along that data structure without ever writing recursive code along the data structure!

It's wild, but functional programming really can slice stuff apart in a way that nothing else reliably does. Imagine if instead of you having to write a unique foldl/reduce (or unfold, or even more esoteric things) for your data structures, you could simply get it for free if you write a single function to explain the recursion termination and make your data structure a functor.