Fin _ is one of those data types that makes you take a
step back and question how much you really understand typed functional
programming.
data Fin : (n : Nat) -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
At first glance so a simple and similar to Nat, yet it
so much more. Like Nat, this is a recursive type with a
base case FZ and a recursive case FS. Also
notice that unlike Nat, this is a dependent type.
Fin _ requires a n : Nat in order to
construct a type. In the FZ case that Nat must
be be S k, that is to say it must be greater then zero. In
the recursive case FS, we provide a Fin k and
yield a Fin (S k), a Fin _ larger by one.
Edwin Brady describes Fin _ as the type of Finite
Sets. That is not to say that Fin _ is a container,
but rather that it represents the canonical set of unnamed elements.
λΠ> the (Fin 1) FZ
FZ
λΠ> :t the (Fin 1) FZ
the (Fin 1) FZ : Fin 1
Here we have FZ as the zero element of the one element
set. FZ requires a S k so this is the smallest
possible finite set we can represent. We can represent the zeroth
element of larger set by simply declaring it so:
λΠ> the (Fin 12) FZ
FZ
λΠ> :t the (Fin 12) FZ
the (Fin 12) FZ : Fin 12
We use FS to construct subsequent elements of our finite
set. For example, the second element of the two element set would
be:
λΠ> the (Fin 2) (FS FZ)
FS FZ : Fin 2
λΠ> :t the (Fin 2) (FS FZ)
the (Fin 2) (FS FZ) : Fin 2
FZ must be of type Fin (S k) and
FS is Fin n -> Fin (S
n). Thus FS FZ produces type
Fin (S (S k)) and k must be Z in
order to match our ascribed type Fin 2.
Let's try to produce an element larger then the ascribed set:
λΠ> the (Fin 1) (FS FZ)
(interactive):1:14--1:19:When unifying Fin (S (S ?k)) and Fin 1
Mismatch between:
S ?k
and
0
at:
1 the (Fin 1) (FS FZ)
^^^^^
Here we tried to produce a second element of the one element set.
Idris is telling us that the only way to construct FS FZ : Fin
1 would be to have FZ : Fin 0. This would allow
FS to type check correctly as Fin 1, however
by the definition of Fin _, FZ : Fin 0 is
impossible as FZ must have type S k.
One natural use case for Fin _ is type safe indexing
into Vect:
index : Fin len -> Vect len elem -> elem
index FZ (x::xs) = x
index (FS k) (x::xs) = index k xs
Fin _ and Vect are parameterized by
len : Nat. This means that we cannot construct
Fin values which are out of bounds for our
Vect. Out of bounds indices are literally unrepresentable.
In my last blog post we took advantage of this property to create a
Representable Functor.
λΠ> index 2 (the (Vect 3 String) ["foo", "bar", "baz"])
"baz"
λΠ> index 3 (the (Vect 3 String) ["foo", "bar", "baz"])
(interactive):1:7--1:8:Can't find an implementation for IsJust (integerToFin 3 3) at:
1 index 3 (the (Vect 3 String) ["foo", "bar", "baz"])
^
The error messaging in Idris2 is a lot less clear then Idris1, but
this is saying that there is not a valid way to convert a
3 : Nat into a Fin 3.
Another interesting use case for Fin _, and the main
topic of this blog post, is Modular Arithmetic where the
Fin _ upper bound is the modulus.
The basic idea is that we perform addition using recursion similiar
to Nat arithmetic, however when we hit the upperbound we
continue the operation from FZ.
We might be tempted start our add function like
this:
add : Fin n -> Fin n -> Fin n
add FZ y = y
add (FS x) y = FS (add ?hole1 ?hole2)
This leaves us with two typeholes:
- + Fin.hole1 [P]
`-- x : Fin k
y : Fin (S k)
0 n : Nat
-----------------------
Fin.hole1 : Fin k
- + Fin.hole2 [P]
`-- x : Fin k
y : Fin (S k)
0 n : Nat
-----------------------
Fin.hole2 : Fin k
add requires two Fin (S k) terms. We have
pattern matched on the first argument and peeled off an FS,
leaving us with x : Fin k and
y : Fin (S k).
What we want to do here is make a recursive call on
add x y applied to FS. This will recurse
through the first argument and accumulate FS constructors
until you hit the base case just like Nat addition.
Fin n = Fin (S k) but because we wrapped our recursive
call in an FS, we only need to fill the holes with a
Fin k. x : Fin k fits perfectly as is, however
y : Fin (S k) has too weak of bounds. We need to
strengthen (reduce in size) the bounds by one so that it fits
the hole.
Strengthening the bounds means reducing the upper limit on a
Fin (S
k) to Fin k. This is only possible if the actual
value is not the upper bound of the set.
Since this is modular addition, what we want to do is strengthen the
bound on y if possible and if it is not possible then we
are at the modulus and must replace y with
FZ.
add : Fin n -> Fin n -> Fin n
add FZ y = y
add (FS x) y =
case ?strengthen y of
Left _ => ?weaken x
Right y' => FS (add x y')
In the case where we wrap around the modulus, we must weaken
the constraint on x : Fin k to account for the fact that we
removed an FS from x in the pattern match but
aren't wrapping an additional FS in the result.
- + Fin.strengthen [P]
`-- x : Fin k
y : Fin (S k)
0 n : Nat
-------------------------------------------------
Fin.strengthen : Fin (S k) -> Either ?_ (Fin k)
- + Fin.weaken [P]
`-- x : Fin k
y : Fin (S k)
0 n : Nat
---------------------------------
Fin.weaken : Fin k -> Fin (S k)
If we have a way to strengthen and weaken our upper
bounds along with a way to detect if we are at the max bound of our
Fin _ then we can implement our add
function.
weaken : {n : Nat} -> Fin n -> Fin (S n)
strengthen : {n : Nat} -> Fin (S n) -> Either (Fin (S n)) (Fin n)
weaken takes any Fin _ and increases its
upper bound. This operation is valid for any Fin _
value.
strengthen takes a Fin (S n) and reduces
the upper bound if possible. If our term x is the
upper bound for Fin (S n) then we cannot reduce it. To get
around this we return an Either where the Left
case returns the original bound. This allows us to use
strengthen for manipulating our bounds and detecting when
we need to wrap around the modulus.
weaken : {n : Nat} -> Fin n -> Fin (S n)
weaken FZ = FZ
weaken (FS k) = FS (weaken k)
For weaken we recurse through the Fin
structure and rebuild it with the weakend bounds.
strengthen : {n : Nat} -> Fin (S n) -> Either (Fin (S n)) (Fin n)
strengthen {n = Z} FZ = Left FZ
strengthen {n = (S k)} FZ = Right FZ
strengthen {n = Z} (FS _) impossible
strengthen {n = (S k)} (FS x) = case strengthen x of
Left l => Left (FS' l)
Right r => Right (FS' r)
strengthen is a bit more complex and requires us to use
the implicit Nat value from the type signature. Lets go
through the cases one at a time:
{n = Z} FZ: We have pattern matched on the zeroeth
element of the Fin (S Z) set which means we cannot
strengthen and must return FZ : Fin (S Z).{n = (S k)} FZ: We have pattern matched on the zeroeth
element of the Fin (S k) set. k cannot be
Z due to the previous pattern match so the set must be size
2 or greater allowing us to strengthen.{n = Z} (FS _): This case is impossible to reach
because FS _ by definition cannot have type
Fin n.{n = (S k)} (FS x): Here we have pattern matched on a
FS with a valid Fin n type. We want to recurse
through the Fin's structure until we hit FZ to
determine if we can strengthen.We now have the tools we need to finish add:
total
add : Fin n -> Fin n -> Fin n
add FZ y = y
add (FS x) y =
case strengthen y of
Left _ => weaken x
Right y' => FS (add x y')
Here you can see (2 + 3) mod 10 = 5 and
(2 + 9) mod 10 = 1:
λΠ> add (the (Fin 10) 2) (the (Fin 10) 3)
FS (FS (FS (FS (FS FZ)))) : Fin 10
λΠ> add (the (Fin 10) 2) (the (Fin 10) 9)
FS FZ : Fin 10This implementation works but lets take this opportunity to generalize our recursion a bit. This will make it easier to implement the rest of our modular arithmetic api.
We can tease apart the recursion from the addition by identify the
Recursion Principle at play in our recursive data type and introducing
an eliminator function for it. This will allow us to write simple non
recursive functions which we can apply to the recursion principle to
deconstruct our Fin _ values and produce some result.
The Recursion Principle for a recursive type is a function
(t : Type)
-> r which deconstructs a value of t : Type into
some r. The Recursion Principle captures the essence of a
recursive function on t and will recursively call itself on
every layer of t inside of t.
This allows us to traverse through the structure of t
and use some other non-recursive function(s) to accumulate
r. The shape of these non-recursive functions is based on
the constructors for t and their signatures can be derived
mechanically.
We do this by replacing all recursive references to t in
the constructor definitions with r and then for each
constructor write a function from its modified parameters to
r.
Lets use
foldr : (a -> r -> r) -> r -> List a -> r as
an example. Looking at the definition of List a:
data List a = Cons a (List a) | NilWe can start with Nil and say that in order to eliminate
Nil we need a function () -> r. Since this
is isomorphic to r, we can simply call this
r.
For Cons we have a pair of a and
List a. We replace all recursive instances with
r leaving us with (a, r) -> r, or
a -> r
-> r in curried form.
Now we pass in those two functions as parameters to our recursive
function returning r and we get
foldr : (a -> r -> r) -> r -> List
a -> r!
We can also write the Recursion Principles for Nat and
Fin:
data Nat = Z | S Nat
total
nat_rec : (r -> r) -> r -> Nat -> r
nat_rec f r Z = r
nat_rec f r (S k) = nat_rec f (f r) k
data Fin : (n : Nat) -> Type where
FZ : Fin (S k)
FS : Fin k -> Fin (S k)
total
fin_rec : {n : Nat} -> (r -> r) -> r -> Fin r -> a
fin_rec {n = Z} f x y impossible
fin_rec {n = (S k)} f x FZ = x
fin_rec {n = (S k)} f x (FS y) = fin_rec f (f x) y
Notice how if you partially apply Nat (or
Fin) they look like church numerals. In some sense you can
say that the Recursion Principle for a type is equivalent to that
type.
Also notice that fin_rec and nat_rec are
total. Since they take non-recursive functions as parameters this means
that whatever functions we implement with our Recursion Principles will
also be total.
The basic idea of how to use fin_rec is that it will
recursively call the r -> r function on the
r value as it traverses through the Fin
constructors. eg., if we have Fin 7 then
r -> r will be applied 7 times.
Armed with fin_rec we now have the ability to recurse
over Fin _ values in a way we know will terminate.
For modular addition we want to specialize r to
Fin n and use a function Fin n -> Fin n
which increments our intial Fin n value by one and which
accounts for the modulus.
total
inc : {n : Nat} -> Fin n -> Fin n
inc {n = Z} x impossible
inc {n = (S k)} x = case strengthen x of
Left l => FZ
Right r => FS r
Then we kick off our fin_rec call with the second
Fin n as the initial value and we are done!
total
add : {n : Nat} -> Fin n -> Fin n -> Fin n
add x y = fin_rec inc y x
This function will add 1 to y x many
times!
Just as with Nat, multiplication is defined in terms of
addition. We use fin_rec with a partially applied
add y to add y to FZ
x times.
total
mul : {n : Nat} -> Fin n -> Fin n -> Fin n
mul {n = Z} x y impossible
mul {n = (S k)} x y = fin_rec (add y) FZ x
We have to pattern match on the implicit value here to prove that the
n = 0 case is impossible because of the explicit
FZ value.
In ordinary arithmetic inversion means to find x for
some y such that y + x = 0. For example,
2 + (-2) = 0. It works the same way in modular arithmetic
but the results can be a little confusing.
Suppose are working with modulus 5 and we want the inversion of 2.
This would be 2 + 3 = 0 (mod 5), making the inversion of 2
to be 3!
A simple way of calculating this is to count down from the modulus value until you hit the number to be inverted. The count will be the inversion.
If we had a function
decr : {n : Nat} -> Fin n -> Fin n that behaved
exactly like inc but it decremented by 1 then we could use
fin_rec to decrement down from the modulus x
times where x is the number we wish to invert.
-- return the largest element in a Fin
total
last : Fin (S n)
last {n = Z} = FZ
last {n = (S k)} = FS last
decr : {n : Nat} -> Fin n -> Fin n
decr {n = 0} x impossible
decr {n = (S k)} FZ = last
decr {n = (S k)} (FS x) = weaken x
total
inv : {n : Nat} -> Fin n -> Fin n
inv {n = 0} x impossible
inv {n = (S k)} x = fin_rec decr FZ x
λΠ> inv (the (Fin 5) 2)
FS (FS (FS FZ))
And there we have it. Our modular arithmetic library:
total
inc : {n : Nat} -> Fin n -> Fin n
inc {n = Z} x impossible
inc {n = (S k)} x = case strengthen x of
Left l => FZ
Right r => FS r
decr : {n : Nat} -> Fin n -> Fin n
decr {n = 0} x impossible
decr {n = (S k)} FZ = last
decr {n = (S k)} (FS x) = weaken x
total
fin_rec : {n : Nat} -> {a : Type} -> (a -> a) -> a -> Fin n -> a
fin_rec {n = Z} f x y impossible
fin_rec {n = (S k)} f x FZ = x
fin_rec {n = (S k)} f x (FS y) = fin_rec f (f x) y
total
add : {n : Nat} -> Fin n -> Fin n -> Fin n
add x y = fin_rec inc y x
total
mul : {n : Nat} -> Fin n -> Fin n -> Fin n
mul {n = Z} x y impossible
mul {n = (S k)} x y = fin_rec (add y) FZ x
total
inv : {n : Nat} -> Fin n -> Fin n
inv {n = 0} x impossible
inv {n = (S k)} x = fin_rec decr FZ x
Writing proofs for associativity, commutivity, etc of modular arithmetic is rather complex and will have to be explored another day.