# Fin, Vect and restrict in idris

--

It seems like a bit of a trap that restrict yields Fin (S n) for a Vect (S n) but it’s giving a type level protection from trying to access a member of a Vect with zero elements (as mod used under the hood is not total for 0 anway). It’s fair enough when you’re putting a function at the top level, as you can capture one less than the Vect’s length in an implicit param like this:

`prepend_to_group : {tsm1 : Nat} -> (rsize : Nat) -> Nat -> Vect rsize x -> Vect (S tsm1) x -> Vect (S rsize) x`

tsm1 is captured structurally as one less than the length of the vect, so restrict can use this value.

But what if you’re implementing a typeclass method like this?

`interface ContainsBytes a where`

get_byte : a -> Nat -> Nat

Vect (S l) Nat is a natural fit for this:

`implementation ContainsBytes (Vect (S l) Nat) where`

get_byte a n = ?get_byte_of_vect_impl

But there’s a problem: we don’t actually have an implicit available for the length of the Vect. Structurally, we’ve guaranteed that the problem can be solved, but some proof machinery is needed, otherwise:

`Can’t solve constraint between: pred (length a) and l`

I needed two proofs, and admittedly I tend not to be an exhaustive reader, so it’s possible the analog of at least the first of these is waiting in the standard library and I wasn’t able to locate it:

`vectLengthIsL : {ll : Nat} -> (v : Vect ll x) -> length v = ll`

vectLengthIsL Vect.Nil = Refl

vectLengthIsL (Vect.(::) _ rest) =

rewrite vectLengthIsL rest in

Refl

Fairly straightforward proof that l = length (Vect l v) … that allows us to recover what would have been the implicit argument and swap (length v) for it.

The other proof target we need is to allow us to replace ll with S (pred ll). Since it’s greater than one we know that’s possible:

`ifVectLenIsSLThenPredVectLenIsL : {ll : Nat} -> (v : Vect (S ll) x) -> pred (length v) = ll`

ifVectLenIsSLThenPredVectLenIsL v =

rewrite vectLengthIsL v in

Refl

Since the type is recoverable, we can use vectLengthIsL to rewrite (length v) as (S ll) in context and rewrite ll as pred (length v), giving the resulting Fin a type describing the number we have.

The result was type rewriting that got us where we wanted to be:

implementation ContainsBytes (Vect (S l) Nat) where

get_byte a n =

let

lastElementOf : Nat

lastElementOf = pred (length a) indexIntoVect : Fin (S l)

indexIntoVect =

rewrite sym (ifVectLenIsSLThenPredVectLenIsL a) in

restrict lastElementOf (cast n) -- Fin (S (pred (length a)))

in

index indexIntoVect a

A small inconvenience but also a chance to look at how rewriting can allow us to construct a Fin that idris doesn’t initially 100% know belongs to the bounds of the Vect it has.