Notes: 26th June 2026
I don't really know why I'm doing this, but I'm trying emacs again. I used to use it all the time, but in 2012 I switched to vim for a month and I'm still there. The lure of the Idris mode in emacs is perhaps too much, and experience so far is that it is nice to not have to leave the editor window much. It did only take me four days to crack and switch on evil mode though (the vim emulation) because there's some things that my fingers just know how to do much quicker that way.
Anyway. Other things. I have discovered, as far as the new core implementation goes, that I'm making it unnecessarily complicated by putting local definitions in the context and indexing the context by the scope. Sure, it can work that way, but there's a lot of gadgets needed to, for example, weaken local definitions, and to make sure we're only doing so when we need to. Instead, we hang on to them where needed, which is during elaboration and evaluation. For evaluation, we hold the values that the local definitions evaluate to. For type checking/elaboration, we hold on to their types. It means passing another thing around when we need it, but it also saves building a load of gadgets for manipulating the global context every time we go in to a new scope, which is often (every time we go under a binder, or a case branch). After all that, I have the evaluator done using a "glued" approach, meaning we have lots of control over what actually needs to get evaluation - which includes local definitions, that we can avoid looking at if they're not needed. Not that it's well tested yet, especially not the evaluation of local definitions! It's going to be tricky to do that properly until I have at least a good chunk of a core type checker written (fortunately, we don't need a full elaborator for that) since I don't particularly want to be constructing programs by hand that are big enough to be interesting.
Also doing some reviewing for TyDe 2026, and next week I'll be giving a talk on Unsoundness in Idris at the Unsound workshop which is part of ECOOP. I've been thinking a bit about what I actually want to say. Hopefully I'll have worked out more precisely what that is by next Tuesday...