# Idris notes: Fin

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… No, not that Idris.

My first stumbling block has been that the signature and constructors for `Fin` are pretty weird.

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?