# 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…

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?