Any notes on normalization by evaluation for dhall-haskell?


#1

I’m currently considering weather to continue with work on my new Dhall implementation, or to try to improve performance of dhall-ruby more before I do so that hopefully the new one can also benefit.

I have done some lower-hanging fruit, but really if I’m serious about this I expect the NbE style that dhall-haskell has switched to will yield an even better speedup when basic operations are slower (as is the case in most scripting language targets). I’m wondering if there are any good notes / thoughts around about this approach that I should be reading (besides the dhall-haskell source and possibly commit messages of course).


#2

I just want to say I am looking forward to NbE in Haskell to crib ideas for dhall-golang too :slightly_smiling_face:


#3

I’d like to mention that @AndrasKovacs’s has a few repositories containing tutorial implementations of normalization-by-evaluation in Haskell:

The core idea behind normalization-by-evaluation is that you encode lambdas from the “guest” language (e.g. Dhall) as lambdas in the “host” language (e.g. Haskell) so evaluating function application in the guest language is the same thing as evaluating function application in the host language (which is fast because the host language is presumably well-optimized).

This paper was how I first learned about this idea, and it introduces a lot of useful concepts and terminology (like “quoting”):

https://www.andres-loeh.de/LambdaPi/

You can also see the core idea behind it here:

That snippet is essentially what @AndrasKovacs did to speed up the normalizer for dhall-haskell, just extended to the full syntax tree.


#4

http://davidchristiansen.dk/tutorials/nbe/