When Conor McBride sets you homework…

The problem given is to write (in Idris) a function satisfying this signature:

1 |
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:

1 |
tabulate f {n=Z} = [] |

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:

1 |
tabulate f {n=S Z} = f fZ :: [] |

Ideally we would like to generate the right-hand 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:

1 2 |
restrict : (Fin (S n) -> a) -> (Fin n -> a) restrict f = \p => f (weaken p) |

`weaken`

is defined in Prelude.Fin, as follows:

1 2 3 4 |
||| 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:

1 |
tabulate f {n=S Z} = f fZ :: tabulate (restrict f) |

Nearly there! Let’s try the more general case:

1 |
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:

1 2 3 4 |
||| The largest element of some Fin type last : Fin (S n) last {n=Z} = fZ last {n=S _} = fS last |

So that gives us:

1 2 3 4 5 |
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`

:

1 2 3 4 |
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.

It seems simpler to tabulate the elements of Fin n then map over them. For example:

fins : Vect n (Fin n)

fins {n=Z} = []

fins {n=S m} = fZ :: map fS fins

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

tabulate f = map f fins

We can test this by tabulating the identity function:

restrictTo : (n : Nat) -> (Fin n -> a) -> (Fin n -> a)

restrictTo _ f = f

> tab (restrictTo 3 id)

[fZ, fS fZ, fS (fS fZ)] : Vect 3 (Fin 3)

Your definition of elements in terms of tabulate is good. If there is an identity function in the library, that might serve just as well as your locally defined fins.

Your definition of tabulate will certainly suffice from the point of view of listing all outputs of the function. However, you have made the task more complex than it needs to be, and also strayed a little from the original idea of inverting the index function from the tutorial so that

index i (tabulate f) = f i

In particular, you should have

index i (elements n) = index i (tabulate id) = id i = i

That would only hold if elements gives the list in increasing order, starting from fZ. Your definition gives the elements in decreasing order, but it certainly catches them all.

Your analysis of the Z and (S Z) cases are correct. Yes to

tabulate {n=Z} f = []

but things get tough in your step up from (S Z) to a general (S k). Yes to

tabulate {n=S k} f = f ?what_goes_here :: tabulate (restrict f)

But no to “We can’t just use fZ every time”! The requirement to invert index tells you that you should use fZ every time! And you can indeed use fZ every time… if you modify your definition of restrict.

You’ve given “last” and a restrict via “weaken”, which gives you “all but last”. They’re certainly interesting and useful operations to define and investigate, but they’re more than you need here. How about “first” and “all but first”?

Your construction is almost the thing, except that “last” and “weaken” can and should be replaced by simpler components (with the same types) which you already have lying around.

Aha! (and doh!)

Better still:

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

tabulate f {n=Z} = []

tabulate f {n=S k} = f fZ :: tabulate (f . fS)

Ah, I did “the simplest thing that could possibly work”, passed my test, but didn’t “refactor mercilessly”!

— Unfold “fins” by one step

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

tabulate2 f {n=Z} = map f []

tabulate2 f {n=S m} = map f (fZ :: map fS fins)

— Unfold “map” by one step

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

tabulate3 f {n=Z} = []

tabulate3 f {n=S m} = f fZ :: map f (map fS fins)

— Simplify the double map

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

tabulate4 f {n=Z} = []

tabulate4 f {n=S m} = f fZ :: map (f . fS) fins

— Simplify the explicit-recursion-and-map to just explicit recursion

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

tabulate5 f {n=Z} = []

tabulate5 f {n=S m} = f fZ :: tabulate5 (f . fS)

f . fS FTW!