I’m trying to get fluent with Idris. It’s hard – but really interesting – but *really* hard. As often happens with these things, you gain a little ground in understanding only to find that just beyond the perimeter of your knowledge is a steep cliff face. Every so often you look down, and realise the ground isn’t there…

My first stumbling block has been that the signature and constructors for `Fin`

are *pretty weird*.

1 2 3 |
data Fin : Nat -> Type where fZ : Fin (S k) fS : Fin k -> Fin (S k) |

The concept is not all that hard. `Fin n`

is an abstract finite set of cardinality `n`

. It’s not a container type, like `Set a`

. The set “is” the type; values of the type are elements of the set, which as far as we’re concerned aren’t anything in particular – think of the “dots inside a circle” notation used by Lawvere to denote abstract sets. We’re not interested in what’s “in” a finite set, we’re just interested in its being of a bounded size.

A value of type `Fin n`

is one of `n`

elements – but which? This is where the constructors come into play, by introducing an *ordering* on these elements like that of `Nat`

, the type of the natural numbers. There’s a Peano-like encoding on the naturals: `Z = 0`

, `S Z = 1`

, `S (S Z) = 2`

and so on. Similarly, here, `fZ`

is the “zeroth” element of a finite set of size `k+1`

(it has to be `k+1`

so that we don’t try to construct an element of an empty set). `fS Fin k`

is then the “successor” element of an element of `Fin k`

, and has the type `Fin (S k)`

.

This is a bit odd. Suppose we have `fZ {k=4}`

– the zeroth element of a finite set of five (4 + 1) elements, which has the type `Fin 5`

. `fS (fZ {k=4})`

is then the successor-to-zeroth element of a finite set of *six* elements, having the type `Fin 6`

– in order to obtain the “next” element, we’ve also had to grow the type. On the one hand, this means that we can never obtain a “next” element outside the bounds of a finite set; but on the other, it means that a successor is always “added” to a finite set, rather than simply located within it.

Suppose we wanted, given a bound `n : Nat`

, to generate a vector of size `n`

containing all the values of `Fin n`

. What would that look like?

1 2 3 |
elements : (n : Nat) -> Vect n (Fin n) elements Z = [] elements (S k) = ?what_now |

Here’s my implementation of elements:

elements : (n : Nat) -> Vect n (Fin n)

elements Z = []

elements (S k) = fZ :: map fS (elements k)

I think a good way to get a handle on the way Fin works is to consider the argument to fZ to be “how much is left” to get to the bound. Then, each fS around it removes one S from the eventual index to fZ.

I would be careful in thinking of Fin as _the_ representation of finite sets. Rather, a type Fin n is _a_ representation of a finite set with n elements.

Very elegant! Also I think likely to be very inefficient, but then we

arewarned…I suppose it’s not so useful just to post some code without explaining how to get there. These instructions will assume idris-mode in Emacs, but the vim mode could just as well be used, with slightly different keybindings.

Step 1 was to start with your code:

elements : (n : Nat) -> Vect n (Fin n)

elements Z = []

elements (S k) = ?what_now

When I load the code into Idris, it gives me a list of metavariables. I have:

k : Nat

—————————————-

Test.what_now : Vect (S k) (Fin (S k))

I can see that I’ll need to use the (::) constructor, because that’s the only thing that can produce a Vect (S k) a. So I replace the code with:

elements : (n : Nat) -> Vect n (Fin n)

elements Z = []

elements (S k) = ?hd :: ?tl

giving this list of metavariables:

Metavariables:

Test.hd

k : Nat

———————

Test.hd : Fin (S k)

Test.tl

k : Nat

——————————

Test.tl : Vect k (Fin (S k))

For the head, I can use fZ, because that is an element of Fin (S k) for every k. So I replace ?hd with fZ. The tail case is a bit more interesting. To see what I get from a recursive call, I write this code:

elements : (n : Nat) -> Vect n (Fin n)

elements Z = []

elements (S k) = let next = elements k in fZ :: ?tl

which gives me the following metavariable:

Test.tl

k : Nat

next : Vect k (Fin k)

——————————

Test.tl : Vect k (Fin (S k))

In other words, I have a Vect k (Fin k) and I need a Vect k (Fin (S k)). For all natural numbers n, Vect n is a functor, so I can use map to transform the elements. And the elements are type Fin k, and I need Fin (S k), which the fS constructor does nicely for.

Now I have:

elements (S k) = let next = elements k in fZ :: map fS next

as the last equation, which I can simplify to

elements (S k) = fZ :: map fS (elements k)

by replacing next with its definition.

It’s a good idea to use Fin for things that will get erased – proofy things, rather than programmy things

An exercise I often set is to implement the inverse of “index” (or rather its flipping).

index : Fin n -> Vect n a -> a

is the function which uses the elements of Fin n to “label the positions” in some Vect n a structure.

We should be able to construct a vector by tabulating a function.

tabulate : (Fin n -> a) -> Vect n a

And yes, you will need to inspect n to define the function. It’s rather a lot like elements, in that respect. But it’s (a) more general, (b) slightly easier to write, and (c) less work to run.

The reason it’s easier is slightly subtle. Ah, I see David has replied in the meantime. Good. The trouble is that the tail of an elements list is not an elements list, but rather an elements list fixed up with “map”. However, the tail of a tabulation most certainly is a tabulation. But of what? Of the “tail” of the function.

So here’s a clue-question. Think of (Fin (S n) -> a) as the functional representation of a nonempty vector. How do you extract head and tail?