Hackle's blog
between the abstractions we want and the abstractions we get.

# Fin

Sorry to disappoint - `Fin` here is not French and does not mean I am done bloggine (yet) :)

`Fin` is a type in Idris that represents `Numbers strictly less than some bound. The name comes from "finite sets".` according to the source code here (you might not want to go there yet if you are new to `Fin` or Idris, just like me).

Let's look at its definition.

``````data Fin : (n : Nat) -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
``````

You'll find `Fin` has two constructors, and `FS` is defined recursively in terms of `FZ`. `FZ` is kind of special, its argument must be in the form of `S k`, which means it can never be 0 as 0 cannot be represented as such. This is Idris' way of saying the argument to `FZ` must be greater than 0.

Clever, but nothing fancy, except...

## The first shock

The acute observers will soon find, although this type has a parameter in `(n : Nat)`, neither of its constructors takes any parameter. In another word, we cannot construct a value for this type! (Edit: actually we can, by specifying the value of the implicit parameter, such as `FZ {k=0}`)

Try this in the Idris REPL:

``````Idris> :module Data.Fin
*Data/Fin> FZ
(input):Can't infer argument k to FZ
*Data/Fin> FS
(input):Can't infer argument k to FS
*fin> FS FZ
(input):Can't infer argument k to S, Can't infer argument k to FZ
``````

Because there no way we can construct it, we cannot give the type parameter (yet). What is going on here? How this is useful at all?

## An example

Let's try to understand it with a typical example.

``````import Data.Fin
import Data.Vect

indexFin : {n: Nat} -> Fin n -> Vect n a -> a
indexFin FZ (x :: xs) = x
indexFin (FS s) (x :: xs) = indexFin s xs
``````

Given a `Vect` of length n, the `indexFin` will not take any invalid index that's equal or greater than n, which saves us the blush of index-out-of-range errors. It is called as such:

``````*fin> indexFin 3 [1,2,3,4]
4 : Integer
*fin> indexFin 0 [1,2,3,4]
1 : Integer
*fin> indexFin 3 [1,2,3]
(input):1:10:When checking argument prf to function Data.Fin.fromInteger:
When using 3 as a literal for a Fin 3
3 is not strictly less than 3
``````

Note how Idris converts numerics to `Fin` values, which begs the question, what are 3, 0, 3 in `Fin`?

## A sliver of light

Still with the REPL, let's try this:

``````*fin> the (Fin 4) 3
FS (FS FZ) : Fin 4
``````

Thanks to the `the` keyword, we can specify that `3` is a value of type `Fin 4`!

## Let's try break it

Notice above there is an error message `When using 3 as a literal for a Fin 3, 3 is not strictly less than 3`, which of course tells us that 3 cannot be Fin 3, as confirmed with this:

``````When using 3 as a literal for a Fin 3
3 is not strictly less than 3
``````

Well, if 3 has to be less than a number, sure we are not short of options?

``````*fin> the (Fin 4) 3
FS (FS (FS FZ)) : Fin 4
*fin> the (Fin 5) 3
FS (FS (FS FZ)) : Fin 5
*fin> the (Fin 6) 3
FS (FS (FS FZ)) : Fin 6
``````

OMG... what is going on here? so 3 can be Fin 4, Fin 5 or Fin 6???

Well that's right! The trick is with the type parameter to `Fin` which we never used to construct any `Fin` value - it's left for interpretation.

Take the above example, try to figure out the type of `FZ` in each example?

take `the (Fin 4) 3` as an example. The REPL interprets it as `FS (FS (FS FZ)) : Fin 4`, if we reverse-engineer a bit, `FZ` would have to be `Fin 1`, so `FS FZ` is of type `Fin 2` and so on.

Now your turn to try `Fin 5` and `Fin 6` - and you'll find `FZ` is interpreted as `Fin 2` and `Fin 3` respectively.

Getting closer...

## Finite set

Next let's count how many values can we construct for a certain `Fin` type.

From what limited I have learnt from Idris, is to always try the base case first. so

``````*Data\Fin> the (Fin 0) FZ
(input):1:1-14:When checking argument value to function Prelude.Basics.the:
Type mismatch between
Fin (S k) (Type of FZ)
and
Fin 0 (Expected type)

Specifically:
Type mismatch between
S k
and
0
``````

Well, if `FZ` cannot work, then `FS FZ` won't either. It seems `Fin 0` can have no values. Which makes good sense in the context of our function `indexFin` - an empty `Vect` has no value, thus cannot return anything for any index.

(Hold on - don't you want to try `indexFin` with an empty Vect?)

Let's try `Fin 1`:

``````*Data\Fin> the (Fin 1) FZ
FZ : Fin 1
*Data\Fin> the (Fin 1) (FS FZ)
(input):1:14-18:When checking an application of constructor Data.Fin.FS:
Type mismatch between
Fin (S k) (Type of FZ)
and
Fin 0 (Expected type)

Specifically:
Type mismatch between
S k
and
0
``````

So `Fin 1` can have 1 value only, which is `FZ`, and `Fin 2`, 2 values, `FZ` and `FS FZ`. `Fin 3`, 3. It's all making sense now isnt' it?

## Summary

`Fin` is a clever type that by leaving its type parameter to interpretation, limit the number of values that a certain type can have. There is a good name to call these allowed values: inhabitants.

Well I didn't think it would take me so long to explain `Fin`! But rest assured, it took me much longer to grok the whole thing and reach my WOW moment.

See Fin for an alternative version of the `indexFin` function.