# Idris homework: tabulate

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

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:

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:

`weaken` is defined in Prelude.Fin, as follows:

So we can now rewrite the case where `n = S Z` like this:

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

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:

So that gives us:

My only hesitation here is that Conor said this was an easy exercise. Is the above really the simplest way to do it?

Finally, here’s `elements` rewritten to use `tabulate`:

Again, I’m not sure whether this explicit definition of `fins` is necessary, or whether it could be expressed more concisely.

## 6 thoughts on “Idris homework: tabulate”

1. Chris Warburton says:

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)

2. Conor McBride says:

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.

1. domfox says:

Aha! (and doh!)

1. domfox says:

Better still:

``` tabulate : (Fin n -> a) -> Vect n a tabulate f {n=Z} = [] tabulate f {n=S k} = f fZ :: tabulate (f . fS) ```

3. Chris Warburton says:

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)

4. Conor McBride says:

f . fS FTW!