Edwin Brady

Whitespace in Idris

As a weekend hack, I’ve been implementing the Whitespace programming language, in Idris. You can find it on github. Whitespace, behind the syntax, is a stack based language with unbounded integers and a single global heap, and control flow implemented using labels, conditional jumps, and subroutine calls. There’s no types (just integers for everything) So what do we gain by implementing it in a language with dependent types? It turns out there’s some interesting things we can do, and problems we have to solve:

If nothing else, we get to see how to use dependent types to make assumptions and invariants explicit in the code. Even if those invariants aren’t used to guarantee total correctness, we at least get the type checker to tell us where we’ve violated them. In fact, I avoided a few errors this way and found a couple of missing or badly specified parts of the whitespace tutorial… Perhaps I’ll write more on this at some point…