Loeb's theorem says that you can prove a statement S if you can prove that S is implied by its own provability. It's actually a generalization of Goedel's second incompleteness theorem (let S be a false statement like 0 = 1). I can see something in the article that looks like Loeb's theorem (f (f a -> a) -> f a, reading f as it can be proved that), but I don't know Haskell, so I'm completely lost after that. Can someone explain in non-Haskell terms what's going on?
Probably not, but since no-one else is having a go, I will:
f is “Functor”, which means roughly the same thing as in category theory (but restricted to the domain of Haskell types). I’m guessing it’s possible to construct a Provability functor.
-> in Haskell is just a function. I’ll mention that types and propositions have a structure preserving isomorphism. So “a” is an arbitrary type but you can think of it as an arbitrary proposition.
But equally, this holds true for all Functors, so we can specialise the function to something like
Not really an answer but if you check out provability section of https://en.wikipedia.org/wiki/Löb's_theorem you'll find a formula very similiar to the haskell type, together with a proof in modal logic.
I think one thing it’s super good for is constructing cyclic graphs from flat representations: you don’t need to do cycle detection. (The example in the code, sadly, does need cycle detection and doesn’t have it. I keep meaning to write a follow-up.)
When (from an engineering, not personal curiosity perspective) is it worthwhile to use loeb?
After reading the article for about 15 minutes, I finally understand loeb and it's pretty cool! It's an easy way to actually run a list of lazy-loading statements (functions) in a way that all of them resolve to their eventual values.
That being said, it feels like the function is both too abstract to understand, yet not effective as an abstraction that I can apply to other problems. For a few contrasting examples, reverse_string is not a very abstract function, as it operates on a very concrete operand and produces an effect that's intuitive outside of mathematical theory. On the other end, a hash table is very abstract, but we choose to learn it because it's such an useful solution.
As for loeb, I only understand how to use it to create a spreadsheet, yet it's clearly meant for more than that since it's given such an abstract name. It's also not called evaluate_lazy_functions_on_operands either so it must be more than that too! Is there something I'm missing?
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.
Spreadsheets are basically a dependency resolution system, since you have to inspect all cells to decide the order in which to evaluate them. So perhaps loeb is just that, a sort of a SAT solver.
Loeb's theorem says that you can prove a statement S if you can prove that S is implied by its own provability. It's actually a generalization of Goedel's second incompleteness theorem (let S be a false statement like 0 = 1). I can see something in the article that looks like Loeb's theorem (f (f a -> a) -> f a, reading f as it can be proved that), but I don't know Haskell, so I'm completely lost after that. Can someone explain in non-Haskell terms what's going on?
Probably not, but since no-one else is having a go, I will: f is “Functor”, which means roughly the same thing as in category theory (but restricted to the domain of Haskell types). I’m guessing it’s possible to construct a Provability functor.
-> in Haskell is just a function. I’ll mention that types and propositions have a structure preserving isomorphism. So “a” is an arbitrary type but you can think of it as an arbitrary proposition.
But equally, this holds true for all Functors, so we can specialise the function to something like
(List (List Int -> Int) -> List Int
I hope this helps, it might not.
Not really an answer but if you check out provability section of https://en.wikipedia.org/wiki/Löb's_theorem you'll find a formula very similiar to the haskell type, together with a proof in modal logic.
I wrote an article based on this one: https://colourcoding.net/2018/03/29/marvellous-moeb/
I think one thing it’s super good for is constructing cyclic graphs from flat representations: you don’t need to do cycle detection. (The example in the code, sadly, does need cycle detection and doesn’t have it. I keep meaning to write a follow-up.)
When (from an engineering, not personal curiosity perspective) is it worthwhile to use loeb?
After reading the article for about 15 minutes, I finally understand loeb and it's pretty cool! It's an easy way to actually run a list of lazy-loading statements (functions) in a way that all of them resolve to their eventual values.
That being said, it feels like the function is both too abstract to understand, yet not effective as an abstraction that I can apply to other problems. For a few contrasting examples, reverse_string is not a very abstract function, as it operates on a very concrete operand and produces an effect that's intuitive outside of mathematical theory. On the other end, a hash table is very abstract, but we choose to learn it because it's such an useful solution.
As for loeb, I only understand how to use it to create a spreadsheet, yet it's clearly meant for more than that since it's given such an abstract name. It's also not called evaluate_lazy_functions_on_operands either so it must be more than that too! Is there something I'm missing?
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.
Spreadsheets are basically a dependency resolution system, since you have to inspect all cells to decide the order in which to evaluate them. So perhaps loeb is just that, a sort of a SAT solver.
> since you have to inspect all cells to decide the order in which to evaluate them
I don’t think this is true; evaluation order of a cell with no dependencies or whose dependencies are already resolved shouldn’t matter
Topological sort should be enough for spreadsheets.
> Feeling smart? Let's change that...
If I ever saw a description of Haskell in a nutshell, this is it. YMMV, of course.