How to convince Idris in vector length

Question

Just getting started in Idris (it's Idris 2 if it matters), and stumble upon this problem. I'm trying to implement a function that returns a vector of all the Fibonacci numbers up to given n. Here's the definition so far (it doesn't compile):

fibs : (n : Nat) -> Vect (n + 1) Int
fibs Z = [0]
fibs (S Z) = [0, 1]
fibs (S k) =
    case (fibs k) of
        (x :: y :: xs) => (x + y) :: x :: y :: xs

The error I get is as follows:

Can't solve constraint between:
    S (S ?len)
and
    plus ?_ (fromInteger 1)

The error points to expression (x :: y :: xs).

I understand I need to prove to Idris the length of fibs k will be at least 2, but I fail to understand how to do that, and why it's not obvious from existing definitions. For me it looks like the k in fibs (S k) must definitely be >= 1, because otherwise either fibs Z or fibs (S Z) would match. The length of fibs k where k >= 1 must therefore be >= 2, by definition of fibs : (n : Nat) -> Vect (n + 1) Int. What am I missing and how to express this in Idris?

xash xash · Accepted Answer · 2020-04-06T15:29:55

First 1 + n is easier to reason about for the type checker than n + 1 as plus pattern matches on the left side:

> :printdef plus
plus : Nat -> Nat -> Nat
plus 0 right = right
plus (S left) right = S (plus left right)

So n + 1 in the type definition cannot be reduced without knowing n, while 1 + n can be reduced to S n.

With this alone fibs compiles. But if you want to check if the function is total, you will get:

> :total fibs
Main.fibs is possibly not total due to:
Main.case block in fibs at test.idr:7:10-17, which is not total as there are missing cases

Because the type checker does not look into other clauses, it does not know that fibs (S Z) is already handled elsewhere. Thus in fibs (S k) = case (fibs k) of … k could be Z, and the result then Vect (S Z) which is not handled in the case switch.

But the fix is as easy as the first one, just pattern match on S (S k):

fibs (S (S k)) = case (fibs (S k)) of
    (x :: y :: xs) => (x + y) :: x :: y :: xs

How to convince Idris in vector length

1 Answers