Idris homework: tabulate

When Conor McBride sets you homework

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?

(edit: see the comments!)

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. 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. 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. Aha! (and doh!)

      1. Better still:

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

  3. 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)

Comments are closed.