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:
- Various operations are only valid if the stack is in the right form (e.g. arithmetic requires at least two items at the top of the stack, and leaves at least one item). We can often statically check that the stack is in the right form before executing such instructions, and at least statically check that the necessary dynamic checks are carried out.
- We need to consider how to represent the stack – a
Stack nis the type of stacks with at least
- There’s a lot of bounds checking of stack references, and as much of this as possible is made static.
- A jump is only valid if the given label is defined. We can statically check this, too, and guarantee that a program we execute has well-defined labels.
- Although whitespace is Turing complete, we can still use the totality checker to verify that executing individual instructions terminates.
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…