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!http://colimit.net/posts/normalisation-by-evaluation/ …
-
Show this thread
-
Replying to @evertedsphere @mrkgrnao
You've got a "TODO how?" in there :-)
1 reply 0 retweets 0 likes -
Replying to @d_christiansen
I think I'll leave that in until I understand that part to my satisfaction haha
1 reply 0 retweets 0 likes -
Replying to @evertedsphere @mrkgrnao
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.
1 reply 0 retweets 2 likes -
Replying to @d_christiansen @mrkgrnao
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?
1 reply 0 retweets 1 like -
Replying to @brendanzab @mrkgrnao
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 :-)
1 reply 1 retweet 2 likes -
Replying to @d_christiansen @mrkgrnao
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.
4 replies 0 retweets 1 like -
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)
2 replies 0 retweets 2 likes -
Replying to @rob_rix @brendanzab and
Haven't read the OP properly yet (I will!), but I just want to add that it looks very much like how Idris 2 evaluates, and that basically never substitutes during unification. Because, as you say, it hurts...
1 reply 0 retweets 5 likes
So it uses indices throughout, and never looks inside a value unless it really needs to.
-
-
Replying to @edwinbrady @rob_rix and
Yeah, the levels+indices approach mentioned here is used in smalltt from what I've seen, which seems to be what you're doing in Idris 2!
0 replies 0 retweets 1 likeThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.