Advent of bugs
Near the start of january, after bumping into some ecosystem issues and lack of a personal support library while working on the 2024 Advent of Code in Idris, I started working on a project to solve all of the Advent of Code problems from all the years in a single massive entirely literate Idris project and publish it as an mdbook. I'm calling it Idris 2 by Extremely Contrived example.
The Good
This has been an amazingly fun project so far. AoC problems are nice and bite sized, giving really good material to work with for incrementally introducing more and more complex concepts. I have been following a sort of "weirdness budget" for each day's solutions, letting myself build on the already established weirdness from previous days. So far I'm 13 days in, and I've already had excuses to introduce all sorts of fun concepts, effects, dependent pattern matching, indexed type families, and refinement types, just to name a few.
Functional programming languages are a lot of fun to model puzzle problems in to start with, but the new design space afforded by dependent typing offers a new, wonderfully fun challenge of figuring out just what to show off while I'm solving the puzzle. There have already been a few problems that I've wound up spending a few days on just tweaking and refining until I was pleased with the balance between weirdness expenditure and showing off what I want to show off in a reasonably approachable way.
A couple of personal favorites of mine so far have been the JSON
parser, and the Digits
views. The JSON parser is written in a bespoke mini-library for
doing effectively parsing that I created just for this project, and
refining the library to optimize for readability of the parsers written
in it was an absolute joy. The digits views allowing pattern matching on
normal integers as if they were lists of digits was less fun to write1, they are amazingly fun to use.
The Bad
I've had to write a lot of support code already. I can't really fault the language, its a pretty new language in its pre-1.0 stage, in a pretty niche area, dependent types are still quite scary to the majority of programmers, and ecosystem improvement was a major goal of the project going in. I have already had to write several "basic" data structures, and there's no sign the need to do so will let up anytime soon2.
Honestly the most painful part has been the lack of support for Idris in external tooling. Essentially every syntax highlighting library has completely ass support for Idris. I managed to eventually sneak proper semantic highlighting into mdbook, it even plays nice with mdbook themes, but I had to commit horrible, horrible crimes to get this working3.
The Ugly
This isn't exactly a complaint, after all, ecosystem improvement was
a goal after all, but I've already run into 2 or 3 compiler bugs, a bug
in the pack package manager, and a weird behavior in katla
that's a maybe bug.
I busted the part of the compiler that automatically inserts
force and delay calls to make interaction
between lazy and strict code Just Work™: idris-lang/Idris2#3461.
I had initially thought I had discovered just one compiler bug,
but it turns out I also stumbled into an unrelated issue in the
termination checker!4
I also found a convoluted hole in the case generator that I had to reach out to the community for help minimizing (thank you dunhamsteve!):idris-lang/Idris2#34665
I broke the pack package
manager by, apparently, being the first person to try and upload a
library to pack-db with library code in literate files, in
my Structures
package, checking in a new data structure motivated by my advent
project, completely breaking the automated docs generation: stefan-hoeck/idris2-pack!319.
This one was especially wild to me, with how popular literate programs
are in the community, I would have never expected to be the first person
to try this.
Looking Forward
Despite the challenges, this has been a lovely experience so far. I greatly look forward to pressing through to completion, whatever it may bring, and have a trophy case full of bugs identified/fixed and new libraries to bring to the ecosystem.
While perfectly understandable, it's not reasonable to expect the compiler to be able to reason about primitive "machine" integers like this on its own, needing to resort to so much
believe_meon this one did make me a bit sad↩︎Well well well, if it isn't the consequences of my actions↩︎
Do not look at the
build-bookscript if you value your sanity↩︎Before anyone gets upset here, despite the name, the termination checker doesn't actually solve the halting problem. It only automatically accepts a subset of the language for which termination is a 'trivial' property, which includes most code I've written in the language so far, but not nearly all of it.↩︎
It's me, I'm the user on the discord↩︎