When Conor McBride sets you homework…
The problem given is to write (in Idris) a function satisfying this signature:

tabulate : (Fin n > a) > Vect n a 
That is, given a function that will provide a value of type a
for every value of type Fin n
, construct a vector of all the possible outputs of this function.
We might think that in order to do this we have to generate all possible inputs to the function – the range of possible values of Fin n
. It is of course possible to do this, but the approach I’ve taken here is slightly different.
Let’s start with the “zero” case. A function (Fin Z > a)
can accept no input, as Fin Z
has no elements. The tabulated vector of its outputs will therefore be empty:
What about a function (Fin 1 > a)
? There exists only one value of type Fin 1
, fZ {k=1}
. We can therefore construct our vector like this:

tabulate f {n=S Z} = f fZ :: [] 
Ideally we would like to generate the righthand side through a recursive call to tabulate, but that means we need a way to convert Fin (S Z) > a
into Fin Z > a
. Let’s write that function in its general form:

restrict : (Fin (S n) > a) > (Fin n > a) restrict f = \p => f (weaken p) 
weaken
is defined in Prelude.Fin, as follows:

 Weaken the bound on a Fin by 1 weaken : Fin n > Fin (S n) weaken fZ = fZ weaken (fS k) = fS (weaken k) 
So we can now rewrite the case where n = S Z
like this:

tabulate f {n=S Z} = f fZ :: tabulate (restrict f) 
Nearly there! Let’s try the more general case:

tabulate f {n=S k} = f ?what_goes_here :: tabulate (restrict f) 
We can’t just use fZ
every time – what we need instead is to pick a value of type Fin n
for each value of n
. The obvious thing to do is to take the “last” element, rather than the “first”. Again, this is defined for us in Prelude.Fin:

 The largest element of some Fin type last : Fin (S n) last {n=Z} = fZ last {n=S _} = fS last 
So that gives us:

tabulate : (Fin n > a) > Vect n a tabulate f {n=Z} = [] tabulate f {n=S k} = f last :: tabulate (restrict f) where restrict : (Fin (S n) > a) > (Fin n > a) restrict f = \p => f (weaken p) 
My only hesitation here is that Conor said this was an easy exercise. Is the above really the simplest way to do it?
(edit: see the comments!)
Finally, here’s elements
rewritten to use tabulate
:

elements : (n : Nat) > Vect n (Fin n) elements _ = tabulate fins where fins : {n : Nat} > Fin n > Fin n fins a = a 
Again, I’m not sure whether this explicit definition of fins
is necessary, or whether it could be expressed more concisely.
Like this:
Like Loading...