Idris notes: Fin

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…

Picture of Idris Elba
No, not that Idris.

My first stumbling block has been that the signature and constructors for Fin are pretty weird.

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?

6 thoughts on “Idris notes: Fin”

  1. Here’s my implementation of elements:

    elements : (n : Nat) -> Vect n (Fin n)
    elements Z = []
    elements (S k) = fZ :: map fS (elements k)

    I think a good way to get a handle on the way Fin works is to consider the argument to fZ to be “how much is left” to get to the bound. Then, each fS around it removes one S from the eventual index to fZ.

    I would be careful in thinking of Fin as _the_ representation of finite sets. Rather, a type Fin n is _a_ representation of a finite set with n elements.

  2. I suppose it’s not so useful just to post some code without explaining how to get there. These instructions will assume idris-mode in Emacs, but the vim mode could just as well be used, with slightly different keybindings.

    Step 1 was to start with your code:

    elements : (n : Nat) -> Vect n (Fin n)
    elements Z = []
    elements (S k) = ?what_now

    When I load the code into Idris, it gives me a list of metavariables. I have:

    k : Nat
    —————————————-
    Test.what_now : Vect (S k) (Fin (S k))

    I can see that I’ll need to use the (::) constructor, because that’s the only thing that can produce a Vect (S k) a. So I replace the code with:

    elements : (n : Nat) -> Vect n (Fin n)
    elements Z = []
    elements (S k) = ?hd :: ?tl

    giving this list of metavariables:

    Metavariables:
    Test.hd
    k : Nat
    ———————
    Test.hd : Fin (S k)

    Test.tl
    k : Nat
    ——————————
    Test.tl : Vect k (Fin (S k))

    For the head, I can use fZ, because that is an element of Fin (S k) for every k. So I replace ?hd with fZ. The tail case is a bit more interesting. To see what I get from a recursive call, I write this code:

    elements : (n : Nat) -> Vect n (Fin n)
    elements Z = []
    elements (S k) = let next = elements k in fZ :: ?tl

    which gives me the following metavariable:

    Test.tl
    k : Nat
    next : Vect k (Fin k)
    ——————————
    Test.tl : Vect k (Fin (S k))

    In other words, I have a Vect k (Fin k) and I need a Vect k (Fin (S k)). For all natural numbers n, Vect n is a functor, so I can use map to transform the elements. And the elements are type Fin k, and I need Fin (S k), which the fS constructor does nicely for.

    Now I have:

    elements (S k) = let next = elements k in fZ :: map fS next

    as the last equation, which I can simplify to

    elements (S k) = fZ :: map fS (elements k)

    by replacing next with its definition.

  3. An exercise I often set is to implement the inverse of “index” (or rather its flipping).

    index : Fin n -> Vect n a -> a

    is the function which uses the elements of Fin n to “label the positions” in some Vect n a structure.

    We should be able to construct a vector by tabulating a function.

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

    And yes, you will need to inspect n to define the function. It’s rather a lot like elements, in that respect. But it’s (a) more general, (b) slightly easier to write, and (c) less work to run.

    The reason it’s easier is slightly subtle. Ah, I see David has replied in the meantime. Good. The trouble is that the tail of an elements list is not an elements list, but rather an elements list fixed up with “map”. However, the tail of a tabulation most certainly is a tabulation. But of what? Of the “tail” of the function.

    So here’s a clue-question. Think of (Fin (S n) -> a) as the functional representation of a nonempty vector. How do you extract head and tail?

Comments are closed.