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 |