juliu.is

Peeling zeroes in Idris

October 28, 2021 • 9 min read

🎶 We’re no strangers to lists, you know the rules and so do I 🎶

Anyway, here’s one:

theBeatles : List String
theBeatles = ["John", "Paul", "George", "Ringo"]

If we want to get an element from a list at a specific index, we can reach for a function like index:

index : Int -> List a -> Maybe a

Which we would use like this:

> index 0 theBeatles
Just "John"

> index 6 theBeatles
Nothing

The reason this function returns a Maybe is that we could pass any number to it. It seems thus inescapable that we need to handle the case when the given number is “out of bounds”. It seems impossible to conjure a function which at the same time is safe and behaves like this:

index : Int -> List a -> a

This seems peculiar because unless something quite monstrous happens we know that there will be no further changes to the Beatles lineup. So the problem is that we know this but the type system doesn’t, and it has to treat that list as it would treat any other list.

Is there no way out?

Enter Idris

In Idris there is another data structure that can describe lists called Vect:

theBeatles : Vect 4 String
theBeatles = ["John", "Paul", "George", "Ringo"]

What’s going on here?

The type also contains information about the length of the list. Let’s see what happens if we forget one of the Fab Four:

theBeatles : Vect 4 String
theBeatles = ["John", "Paul", "George"]

Idris complains:

When unifying Vect 0 String and Vect 1 String.
Mismatch between: 0 and 1.

Test:6:39--6:40
 2 |
 3 | import Data.Vect as Vect
 4 |
 5 | theBeatles : Vect 4 String
 6 | theBeatles = ["John", "Paul", "George"]
                                           ^

Don’t worry too much about the specifics of the error message, just look at that little caret that Idris puts at the end. It’s almost as the compiler is telling us “Hey, something’s missing there”.

With this data structure we can write something like this:

> Vect.index 0 theBeatles
"John"

Note that we get the raw value, no Maybe nonsense here. What about when we pass a number that’s out of bounds?

> Vect.index 6 theBeatles
Error: Can't find an implementation for
       IsJust (integerToFin 6 4).

(Interactive):1:12--1:14
 1 | Vect.index 6 theBeatles

Woah, now the compiler understands. Cool. But what’s the type signature of this index function?

> :t Vect.index
Vect.index : Fin len -> Vect len elem -> elem

Uh, what that’s Fin type? It describes a natural number strictly less than some bound. The name comes from “finite sets”, i.e. sets that have a finite number of elements. Its definition is:

data Fin : Nat -> Type where
  FZ : Fin (S k)
  FS : Fin k -> Fin (S k)

Ok.

We might need to take a little step back to unpack it.

Natura, artis magistra

Natural numbers are integers greater or equal than zero. A neat trick to represent them is to create a recursive type:

data Nat
  = Z
  | S Nat

Where Z represents zero, while S Nat represents the successor of a certain natural number.

Using this type we can construct the following values:

Z           == 0
S Z         == 1
S (S Z)     == 2
S (S (S Z)) == 3

You can see that Idris does a little bit of magic under the hood so that we can write 1 instead of S Z. Neat.

A somewhat interesting fact is that we can also get the previous natural number by removing a layer of S:

prev : Nat -> Maybe Nat
prev Z = Nothing
prev (S x) = Just x
> prev 0
Nothing

> prev 1
Just 0

> prev 2
Just 1

Now that we know how to express natural numbers in Idris, we can take a look at our finite subsets of natural numbers.

The Meat and Potatoes

Let’s look at that definition again:

data Fin : Nat -> Type where
  FZ : Fin (S k)
  FS : Fin k -> Fin (S k)

This looks a tad different from the previous data Nat = Z | S Nat definition, but it’s quite close:

  • We are defining a function called Fin that takes a natural number and returns a type.
  • One possible constructor is FZ, which stands for “finite zero”.
  • The other constructor is FS, which takes an existing Fin and returns its successor.

From this explanation it’s not clear how we are restricting these natural numbers, so let’s play around with some finite numbers. Since a literal 0 can be an Int, a Nat, and many other things, we have to use the special the function to tell Idris which specific type we want:

> the (Fin 1) 0
FZ

So everything is good when we ask for a 0 in Fin 1, the set of natural numbers strictly less than 1. How about this?

> the (Fin 0) 0

It blows up!

Error: Can't find an implementation
for IsJust (integerToFin 0 0).

(Interactive):1:13--1:14
 1 | the (Fin 0) 0

Why is this happening? By definition the minimum value we can create is FZ. The type of this value is Fin (S k), and by definition S k must be greater than zero. So this means that the smallest set we can create is Fin 1, which is the set that only contains zero.

Let’s look at Fin 2, the set that contains 0 and 1.

> the (Fin 2) 0
FZ

> the (Fin 2) 1
FS FZ

As expected, the zeroes in Fin 1 and Fin 2 are different:

> the (Fin 1) 0 == the (Fin 2) 0
Error: When unifying Fin 1 and Fin 2.
Mismatch between: 0 and 1.

(Interactive):1:1--1:14
 1 | the (Fin 1) 0 == the (Fin 2) 0
     ^^^^^^^^^^^^^

Ok, time for a little surprise. Look at these values again:

> the (Fin 2) 0
FZ

> the (Fin 2) 1
FS FZ

Those FZ values are not the same! The first one is of type Fin 2, while the second one is of type Fin 1. This makes sense when we look at the type of the FS function:

FS : Fin k -> Fin (S k)

Or making it more concrete:

FS : Fin 1 -> Fin 2
  • we get a 0 of type Fin 1
  • we apply FS
  • we get a 1 of type Fin 2

How would we get a 2 of type Fin 2? We would need to apply the FS function twice, going from Fin 0 to Fin 1 to Fin 2, right?

The problem is, we simply cannot do that.

The smallest valid finite set is Fin 1, which means we just cannot apply that function twice to create that value. You can only apply it once, giving us 1, which is the largest element in Fin 2.

If we look at Fin 3, things start making more sense:

> the (Fin 3) 0
FZ

> the (Fin 3) 1
FS FZ

> the (Fin 3) 2
FS (FS FZ)

> the (Fin 3) 3
Error: Can't find an implementation
for IsJust (integerToFin 3 3).

(Interactive):1:13--1:14
 1 | the (Fin 3) 3

It’s like we’re starting with this beefy zero, and we need to peel a layer to be able to create the next number. Then we keep peeling and peeling, up until we just can’t peel anything anymore. Fin 1 is the end of all hopes, the last laugh, the final curtain.

And Now for Something Completely Different

If you’ve followed so far, you’re in for a treat 🍭

We’ve talked a lot about Vect and Fin, but you don’t need any of that to reap the benefits we’ve talked about! Let’s go back to lists:

theBeatles : List String
theBeatles = ["John", "Paul", "George", "Ringo"]

Look at this:

> List.index 1 theBeatles
"Paul"

What??? How is it possible it just returns a value, no Maybe in sight?

> List.index 5 theBeatles
Error: Can't find an implementation for InBounds 5
  ["John", "Paul", "George", "Ringo"].

(Interactive):1:1--1:24
 1 | List.index 5 theBeatles
     ^^^^^^^^^^^^^^^^^^^^^^^

Just how. Let’s dig in:

> :t List.index
List.index :
  (n : Nat) ->
  (xs : List a) ->
  {auto 0 _ : InBounds n xs} ->
  a

If we look at the third argument we notice some curly braces around it. I won’t go too much in detail, but that’s an implicit argument that doesn’t need to be passed in when calling the function.

The interesting bit for us is that InBounds type:

data InBounds : Nat -> List a -> Type where
  InFirst : InBounds 0 (x :: xs)
  InLater : InBounds k xs -> InBounds (S k) (x :: xs)

That looks complicated. But how about we compare it to this?

data Fin : Nat -> Type where
  FZ : Fin (S k)
  FS : Fin k -> Fin (S k)
  • There is a base case. We use x :: xs to signal that the list must not be empty, so that we can never get an InFirst value of type InBounds 0 [].
  • There is a function that we can call recursively to peel a layer. In this case, not only do we go from k to S k, but we also specify that the list gets an extra element in front.

If you squint a bit, you’ll see it’s the exact type trick we’ve seen before. If we tried to call List.index 1 ["John"] we’d have to find a way to call the InLater function to peel off a layer. Or more concretely:

InLater : InBounds k xs -> InBounds (S k) (x :: xs)
-- becomes
InLater : InBounds 0 [] -> InBounds 1 ["John"]

The problem is constructing that InBounds 0 []. By definition InFirst has to be InBounds 0 (x :: xs), so we simply cannot create such value. Thus the type system cannot find a valid implementation of InBounds 1 ["John"], which is exactly the error message Idris prints out. QED

I hope you enjoyed this adventure in the land of zeroes and dependent types.

Fin 1.

Profile picture

A blog by Ju Liu.

I try to write code that doesn't suck. I rarely succeed.