Notes: 12th June 2026
More work on the evaluator in the new core. It's interesting how much needs to be done to support local definitions, and thinking about laziness, of weakening and evaluation of let blocks. Why? Firstly: the context, which we pass around everywhere, now contains definitions in the local scope, and not just the global definitions. So, that means in the implementation, it needs to be indexed by the local scope. Not really a big deal, but we do need to make sure that the usual weakening and embedding gadgets are not overly expensive. When we go under another binder, we will need to weaken the locally defined names too. But we may never look at them... so we need to take care to do this lazily. Also, say you're evaluating let x = y in z which results in let x = y' in z', it's likely (but not impossible) that we'll never have to look at y'. We might if, say, we want to print the full result, or continue evaluation (say if z was blocked, awaiting a metavariable solution). But, usually, if we're using the result of evaluation for conversion or unification, we're not going to need it.
Anyway, so that means I've been doing all that plumbing, as well as catching up with the Scottish PL folks at SPLS.
Also: I'm going to a workshop next week, where I'll be giving a talk on reasoning in Idris to some mathematicians who are thinking about AI and proof. I have opinions in that, but it's not for this space :). So I've been spending a bit of time thinking about that, and how to present what Idris even is.