Conversation

Normalisation, how to do it fast for the untyped lambda-calculus by means of evaluation, and why we care (together with some of the required type theory/PLT background): first of a series, hopefully. Feel free to yell at me in replies about mistakes etc! colimit.net/posts/normalis

David Thrane Christiansen

@d_christiansen

Feb 3, 2020

You've got a "TODO how?" in there :-)

swann

@evertedsphere

Feb 3, 2020

I think I'll leave that in until I understand that part to my satisfaction haha

David Thrane Christiansen

@d_christiansen

Feb 3, 2020

Here's my take: with de Bruijn indices, variables need to be incremented when you put them under a new binder. They refer to binding sites relative to their occurrence. Levels refer to them absolutely and thus don't need incrementing under a new binder.

Brendan Zabarauskas

@brendanzab

Feb 3, 2020

My (probably bad) understanding is that the nifty thing about indices is that you can avoid having to rename things. The nifty thing about levels is that you can move around terms without having to shift indices. Combining them together with NbE gets you the best of both somehow?

David Thrane Christiansen

@d_christiansen

Feb 3, 2020

Indices are nicer for writing evaluators (they basically say how far up the stack to look for the value). The way I see it, levels are nice for free variables, and indices for bound variables. Boundness vs freeness depends on your perspective :-)

Replying to

and

The thing that kind of makes me unhappy about the approach is the fact that you have to copy around the entire environment all the time, regardless of if any of it is used. Seems a tad wasteful, but I dunno.

9:57 PM · Feb 3, 2020Twitter Web App

Replying to

and

it’s really *very* expensive traversing trees and substituting a lot too, tho. (in the context of a dependently-typed lang where you’ve probably got higher-order unification, anyway)

Brendan Zabarauskas

@brendanzab

Feb 3, 2020

Oh yeah, I've done that before, it was not nice! Definitely would rather not do that. I'm thinking more about having captures explicit… but I haven't really thought it through. Kind of like contextual type theory I think?

Replying to

and

I also want to eventually be able to look at these terms as graphs and compare them. So, parameters or record fields should be more 'graphy' than 'listy'. Not sure how viable the indices+levels approach is long term for that…

David Thrane Christiansen

Replying to

and

What is fast is not always elegant, and what is elegant is not always fast. Ideally we wouldn't need interpreters at all - see e.g. Grégoir and Leroy's paper on Coq's vm_compute, or Dirk Kleeblatt's thesis. Also ongoing work on Lean 4.

Brendan Zabarauskas

@brendanzab

Feb 3, 2020

Yeah, big fan of the compilation to byte-code stuff! More just lamenting about how nested lambdas/currying seems very ordered/listy when what I really want is to be able to build up graphs of dependencies between things. Still trying to articulate what I mean though.

Show replies

Replying to

and

In a naive Haskell/ML implementation, env copying is just copying a single pointer, which is pretty fast. The drawback though is some space leak, but for reasonable examples it's not an issue.

Brendan Zabarauskas

@brendanzab

Feb 3, 2020

Yeah, I'll believe you - it's a mild annoyance. I think I'm going to have to use immutable data structures for environments (in my Rust implementation). I think my struggle is more to do with how to then progress from there to doing more interesting stuff with dependency graphs.

Show replies