Implementing Löb’s theorem in Emacs Lisp
Back in 2006, Dan Piponi wrote about Löb’s theorem and how it can be implemented elegantly in Haskell and used to build a spreadsheet calculator from a very minimal core. Further notes on the Haskell wiki abstract his loeb function further, and offer a bit more insight into how it operates.
A few years later, as I was working on an evaluator for the Nix language, it occurred to me that the style of recursive evaluation in nixpkgs felt very similar to Dan’s spreadsheet. Based on this, I was able to implement that eva…
Implementing Löb’s theorem in Emacs Lisp
Back in 2006, Dan Piponi wrote about Löb’s theorem and how it can be implemented elegantly in Haskell and used to build a spreadsheet calculator from a very minimal core. Further notes on the Haskell wiki abstract his loeb function further, and offer a bit more insight into how it operates.
A few years later, as I was working on an evaluator for the Nix language, it occurred to me that the style of recursive evaluation in nixpkgs felt very similar to Dan’s spreadsheet. Based on this, I was able to implement that evaluator using a monadic variation of his loeb function, which ended up working out rather simply.
At the time, Emacs had neither threads nor thunks, but in 2015 it gained the latter, which I only realized last week opens the door to implementing loeb — and as a result, nixpkgs-style package evaluation — directly in Emacs Lisp. Here is what it looks like in operation:
(loeb-alist-overlays
'((foo . (lambda (final _parent)
(1+ (loeb-get 'bar final))))
(bar . (lambda (_final _parent)
123)))
'((bar . (lambda (final parent)
(+ 100 (loeb-get 'bar parent)))))
'((foo . (lambda (final parent)
(+ 100 (loeb-get 'foo parent))))
(baz . (lambda (final parent)
(+ 100 (loeb-get 'foo final))))))
==>
((baz . 424)
(bar . 223)
(foo . 324))
You can find the code here, along with versions for plain alists, plists and both vectors and lists. Sadly we don’t have a Functor abstraction as Haskell does, but it should be straightforward to implement a similar scheme for other container-like types as well.