Is there a reason to prefer Peano numbers to type-level arithmetic built in GHC?

Posted on 2017-11-22 by Oleg Grenrus

I was asked: Is there a reason to prefer Peano numbers to type-level arithmetic built in GHC? in the fin and vec -announcement thread on Reddit.

That's a good question.

My answer was:

It can be reprhased into:

  • GHC.TypeLits is magic, and to work with them you'd need more magic
  • Peano numbers provide structural invariants, which are great for type-driven development.

Let's expand the first point. Let's look into vector-sized library, which in the version uses finite-typelits for some parts.

We can create a vector:

and query elements:

The author of finite-typelits chose to error if we try to create invalid Finite number, which is fair choice. So far so good.

Looking at the documentation of vector-sized you may notice the type of izipWith is

You'd want to go all in, and use Finite n there instead of an Int. Luckily, there are building blocks:

so implementing fzipWith is simple:

but imagine, there weren't generate_ available. Then we'd need to implement it:

Note the use of unsafe Finite constructor. As Finite invariant isn't structural you need to verify it manually. As a library writer (you wear a library writer hat, when a library is missing the feature, and you are adding it, either to the original library or in your code), You have to verify that your code is correct by hand. Compiler doesn't help you here.

Compare to the similar function in vec library: there's nothing unsafe (P.Vec n a ~ Fin n -> a):

Not only compiler verifies that code, it also helped writing it. In the process I probably wrote the zero length/empty vector case first:

I'm missing a non-empty list case, let's add one:

and so on. Let's have a dialogue with the compiler.

If I mess up:

Once you get used to typed holes, there is no going back. Don't even try Agda with its C-c C-a or C-c C-r, that's the right kind of magic.

If you are still Agda-curious, watch Conor McBride - SpaceMonads, but than fall back to reading Hasochism: the pleasure and pain of dependently typed haskell programming (similar tiling thing, but in Haskell. Google for PDF), because we write Haskell, don't we? :)

Site proudly generated by Hakyll