104 lines
5.3 KiB
Markdown
104 lines
5.3 KiB
Markdown
# 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](https://adventofcode.com/) 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](https://static.stranger.systems/idris-by-contrived-example/)
|
|
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](https://static.stranger.systems/idris-by-contrived-example/Parser/JSON.html),
|
|
and the
|
|
[`Digits` views](https://static.stranger.systems/idris-by-contrived-example/Util/Eff.html).
|
|
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 write[^1], 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 soon[^6].
|
|
|
|
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 working[^2].
|
|
|
|
## 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](https://github.com/idris-lang/Idris2/issues/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![^8]
|
|
|
|
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#3466](https://github.com/idris-lang/Idris2/issues/3466)[^9]
|
|
|
|
I broke the [pack](https://github.com/stefan-hoeck/idris2-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](https://git.sr.ht/~thatonelutenist/Structures) package, checking in
|
|
a new data structure motivated by my advent project, completely breaking the
|
|
automated docs generation:
|
|
[stefan-hoeck/idris2-pack!319](https://github.com/stefan-hoeck/idris2-pack/pull/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.
|
|
|
|
[^1]: 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_me` on this one did make me a bit
|
|
sad
|
|
|
|
[^6]: Well well well, if it isn't the consequences of my actions
|
|
|
|
[^2]: Do not look at the `build-book` script if you value your sanity
|
|
|
|
[^8]: 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.
|
|
|
|
[^9]: It's me, I'm the user on the discord
|