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:

```
One way to see that is: If you use a library using type-level naturals, than
`GHC.TypeNats` -based would be nicer to use (more convenient, maybe faster).
OTOH, when writing a library, less "magic" is better.
```

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 0.6.1.0 uses `finite-typelits`

for some parts.

We can create a vector:

```
λ> :set -XDataKinds
λ> let vec = generate (\x -> x * x) :: Vector 10 Int
λ> vec
Vector [0,1,4,9,16,25,36,49,64,81]
```

and query elements:

```
λ> index vec 3
9
λ> index vec 11
*** Exception: fromInteger: Integer 11 is not representable in Finite 10
```

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:

```
generate_ :: forall n a. KnownNat n => (Finite n -> a) -> Vector n a
zipWith3 :: (a -> b -> c -> d)
-> Vector n a -> Vector n b -> Vector n c -> Vector n d
```

so implementing `fzipWith`

is simple:

```
λ> let fzipWith f = V.zipWith3 f (V.generate_ id)
λ> :t fzipWith
fzipWith
:: KnownNat n => (Finite n -> b -> c -> d)
-> Vector n b -> Vector n c -> Vector n d
```

but imagine, there weren't `generate_`

available. Then we'd need to implement it:

```
generate_ :: forall v n a. (KnownNat n, VG.Vector v a)
=> (Finite n -> a) -> Vector v n a
generate_ f = Vector (VG.generate i (f . Finite . fromIntegral))
where i = fromInteger (natVal (Proxy :: Proxy n))
```

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`

):

```
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull (P.Vec f) = case N.snat :: N.SNat n of
N.SZ -> VNil
N.SS -> f F.Z ::: fromPull (P.Vec (f . F.S))
```

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

```
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull (P.Vec f) = case N.snat :: N.SNat n of
N.SZ -> VNil
```

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

```
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull (P.Vec f) = case N.snat :: N.SNat n of
N.SZ -> VNil
N.SS -> _h ::: _t
```

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

If I mess up:

```
fromPull :: forall n a. N.SNatI n => P.Vec n a -> Vec n a
fromPull (P.Vec f) = case N.snat :: N.SNat n of
N.SZ -> VNil
N.SS -> f F.Z ::: fromPull (P.Vec f)
```

```
• Could not deduce: (n1 :: Nat) ~ ('S n1 :: Nat)
from the context: ((n :: Nat) ~ ('S n1 :: Nat), N.SNatI n1)
```

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