The “Hello World!” example for fancy type systems is probably the sized vector
append function (“The output has size equal to the sum of the
inputs!”). One the one hand, it is perfect: simple enough to explain without
pages of code, yet complex enough to show off whats cool about dependency. On
the other hand, like the sweater I’m sporting right now, it’s a bit well-worn and
worse, was never wholly convincing (“Why do I care what the size of the
output list is anyway?”)
Recently, I came across a nice example that is almost as simple, but is also well motivated: Okasaki’s beautiful Lazy Amortized Queues. This structure leans heavily on an invariant to provide fast insertion and deletion. Let’s see how to enforce that invariant with LiquidHaskell.