Notes: 22nd May 2026
It's the Idris developer meeting this week! So a chance to get my Research Brain working again after not having had significant stretches of time to think for a while. Although, Monday is spent travelling back from a Thing in Germany, popping between coffee shops and airports and looking over the new Idris code base trying to remember how things work, and how I'm planning to make things work.
And in the end, I deleted lots of things, and started yet another experimental new thing. And it's basically because of this: case blocks in Idris 2 involve a variety of hacks upon hacks, which is deeply unsatisfying, especially when it comes to local definitions (that is, where blocks). I won't go into the reasons why here (except to say that, as always, it's about names and scopes) but my conclusion was that, instead of tweaking detail after detail in the new version, it would be more productive and more fun to rip it all up and start again. So, now I have yet another attempt at implementing the core type theory, this time with case blocks and local definitions as first class features. I have so many changes I want to make to the way things are done - in unification, in elaboration - that this gives me an easier opportunity to actually make those changes throughout.
Now, in the end, this doesn't necessarily mean ripping everything up and throwing all the existing work away. Experience suggests that once the core language works as intended, bringing the high level language back doesn't take very long, and a lot of the existing work is reusable.
Optimising for fun, as always :).