Notes: 24th July 2026
Been a few weeks, sorry! Partly been on the road, partly taking a bit of a break because it's been just too hot. So, just briefly: progress on the new core (currently going by the name LTT3 and I can't even remember why but I'll stick with that as a shorthand until it turns into an actual programming language) continues, working through the basic bits of machinery needed for evaluation, conversion checking and unification. So far nothing too surprising has come up in having to deal with local definitions, so let's hope it continues that way. Also, I got distracted for a few days by thinking about compiling to C via continuations, and looking how Scheme in particular does it. There's some interesting thoughts from Andy Wingo on this topic. We used to compile Idris to C, via defunctionalisation and ANF, and the performance was pretty decent though not as good as the current Chez Scheme based back end. But even so there are possible advantages to going via C, if only for portability and reducing the number of dependencies so maybe I'll revisit properly one day. But not just yet.
I went to the UNSOUND workshop at ECOOP and talked about sources of unsoundness in Idris. I might have talked myself into revisiting universes, which I never got around to implementing in Idris 2. But, again, not just yet, because I really need to get that core working... Anyway, there were plenty of interesting talks at UNSOUND and I particularly enjoyed hearing from Gina Banyard about PHP's type system (no, honestly, it's not an oxymoron...).