Notes: 15th May 2026
I've recently stumbled on the concept of Weeknotes so I thought I'd give it a go. It's mostly to remind myself of progress when I wonder what it is I've even done at some point in the future, but also so that maybe people can see what progress is being made with the new Idris, and to make sure that week to week some progress actually does happen! Rather than the, up to now, constant changing of mind about how to do things. Maybe I'll write about where I'm stuck or where I can't make my mind up about something. They are not intended to be well written, well organised, or even particularly interesting. Let's see how long it lasts. I give it a fortnight but maybe if they're public I'll shame myself into doing it for longer.
Because apparently this needs saying these days: No I'm not getting an LLM to do this. Or anything. For goodness sake. Learn to speak for yourself again. Use your own voice, not the bland average voice of every user that went before you. Use em dashes if you want.
Some context, since this is where it starts. I've been rethinking Idris, because I've been working on it and with it for a while and over the last couple of years, Idris 2 has been in the more than capable hands of a team of volunteers without all that much input from me. I consider this a win :). While they've been doing that, I've been rethinking both the design and implementation, because what I really want from Idris (or indeed any language) is something that is interactive, responsive, where programming is a conversation between developer and machine, in a language that both parties understand and which is formal and clearly and unambiguously defined. (At this point, I ought so say something about LLMs. So that's got that out of the way).
Anyway: I'm working on this new thing (private repo for now). Much as I still like Idris, some design mistakes are obvious in hindsight (honestly some were obvious at the time but I made them anyway). There's too much implicit cleverness, in things like resolving ambiguities, implicit laziness and maybe some bits of syntactic sugar. In the implementation, I don't like that the granularity of the system is per-file, meaning that a small change can lead to a lot of rebuilding. The evaluator often does too much work anyway - I have a new system based on a glued representation of values, which essentially means that you can always see where an evaluated term came from (what did the user write) and have full control over when you evaluate subexpressions which, based on early experiments, seems to have lots of benefits not only in performance but in making error messages clearer since they actually show what the programmer wrote, and not what it might have reduced to at some stage.
So, the new thing is, for the moment, my own little (or not so little) project in which I not only try to address the above, but try to remember that my job is to do research rather than (or maybe as well as) create a product. The current state is an elaborator for the intermediate language, with a new evaluator but quite a bit borrowed from an earlier state of Idris 2. It is, alas, well out of sync with Idris 2 by now, but I'll worry about that later (remember: researcher, not making a product!). Next step is to work through the bits of the elaborator that I find unsatisfying, and this week I've been looking at how the case construct works. Or, maybe more accurately, doing it again, so that we have a dependent pattern matching construct that can appear anywhere in a term, and support the with construct. If this works the way I think it should, it will simplify the elaborator and make it much easier to maintain, which is a large part of the point of this increasingly large exercise. For reasons of grading and travelling I haven't done much more than adding some syntax to the (experimental) implementation and scribbled some notes on paper, but that's a start at least.
Other stuff: nearly the end of semester. Marking of group projects is done! Still have some final year project dissertations to read. Always enjoyable to see what the students have achieved throughout the year.