5 ms·
Löb and Möb: Loops in Haskell (2013)
- gnabgib 1y ago(2013) Popular in: 2021 (153 points, 60 comments) https://news.ycombinator.com/item?id=34578411 https://news.ycombinator.com/item?id=34578411 2018 (86 points, 10 comments) https://news.ycombinator.com/item?id=18159087 https://news.ycombinator.com/item?id=18159087
- anon291 1y agovery useful when writing toy assemblers in Haskell as loeb let's you easily resolve labels to addresses once you've output the other instructions. Also a good use of the tardis monad which does the same thing as loeb but with a bit more panache
- sfvisser 1y agoReminds me of this classic doing the same: http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html?m=1 http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...
- sevensor 1y agoI’ve read the post carefully and I still don’t get how they proved Santa Claus without proving the proposition.
- phplovesong 1y agoUuh i miss the strange loop conference. It was simply the best and most fun programming related conference ever.
- moomin 1y agoThis stuff is really cool; I’ve literally written an article about it myself. However, unless you address the possibility of entering an infinite loop, it’s not really that useful.
- Twisol 1y ago> This shows how moeb is a generalization of fix. To be fair, loeb was already a generalization of fix. If `f` is the identity functor, then `loeb` has type `(a -> a) -> a`, and the `fmap` used in its definition resolves to `id`. It's a shame there aren't any other example applications of moeb. The author mentions using `traverse` and `foldMap`, but those are also based fundamentally on `fmap` in some sense, and I wouldn't be too surprised if they also ended up being literally `fmap` for some specific choice of functor.
- quchen 1y agoI did not expect this to surface after all these years, but here we are! o:-)
- jaapz 1y agoWhats up with all these haskell articles being posted all of a sudden (many of them by quchen)
- tkz1312 1y agomaybe something to do with Haskell being a beautiful and foundational language that has been a major driver of progress in programming language design for the last two decades?
- JadeNB 1y agoI suppose you could argue when it started being a major driver of progress, but it's actually been around for 3.5 decades! https://en.wikipedia.org/wiki/Haskell#Haskell_1.0_to_1.4 https://en.wikipedia.org/wiki/Haskell#Haskell_1.0_to_1.4
- deleted 1y ago[deleted]
- plaidfinch 1y agoTen years ago Dan Piponi's 2006 exploration of this same idea (http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...) inspired me to write the paper "Getting a Quick Fix on Comonads" (https://github.com/plaidfinch/GQFC https://github.com/plaidfinch/GQFC), which ended up in Haskell Symposium 2015. It turns out there's a more powerful and arguably more interesting version of the Löb fixpoint in a setting where we have a ComonadApply, i.e. a structure that's not merely a functor, but also a comonad and comonad's version of Applicative. What emerges looks like spreadsheet evaluation in arbitrarily shaped spaces, with relative references provided by the comonadic structure. I've always found this stuff tremendously fun, and it's a delight that people keep stumbling across it who share my enthusiasm!
- ballpug 1y agogtk-daemons in Gödel's incompleteness theorem, where Löb functor cell value differ from readiness-to-hand and presence-at-hand.