Hiatus

I’m putting my WebGL in Idris project on hiatus. I started this project to get a feeling for how far I could take type-safety using dependent typing. Unfortunately, I am no longer constrained by dependent typing in general, but by Idris in particular. I might continue once significant progress has been made on the Idris compiler.

I’ve spent days debugging problems that turned out to be compiler problems. Error messages are extremely unhelpful. The prelude sometimes gets in the way. The syntax can be hard to read. Linear types exist but are not well-supported. The compiler code base is hard to get in to. Documentation is quite basic. In short, using Idris “in anger” is a pain in the butt, and if your problem requires Idris’ particular feature set, you are probably already very angry. One doesn’t typically use quantitive type theory to increment a counter. Although that is exactly whet I did in the last entry.

I’m not blaming Idris’ devs for these problems. Their scope is large and time limited. Working in academia probably also forces a focus onto e.g. publications rather than nice error messages.

I don’t like ending this project, because I hoped it could unify my love for type-safety with my love for 3D graphics, but after months of development I still only have a spinning white trianle, while I’m considering how supermonads qualified with dependently-typed destructors might allow monadic error handling for linear values if I can get idris to auto-construct destructors for values derived from function application. Needless to say my love for 3D graphics isn’t particularly fulfilled.

However, I did sort-of get my answer.

I’m sold on dependent typing. It is actually easier to use dependent types. At some point there will be something you wish to express that is easy with dependent types, but quite complex otherwise. Dependent types are just doing to types what you are already doing in terms. Not conceptually difficult, just a different way of doing things that takes some “unlearning”.

Linear types on the other hand are an entirely new thing. More research is needed to make them fun to use in practice, but they are already damned useful.