Idris pattern matching on successor (next value)

Question

On the following function I'm pattern matching on the Successor of k on (S k)

vectTake : (n : Nat) -> Vect (n + m) a -> Vect n a
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

Is it possible to use that value on the body of the function if needed?

Another solution would be match on k and use the antecessor of k on the body function, so that just another form of solving the same problem or this kind of pattern matching provides any other advantages that I could not see?

Answer 1

For your first question ...

The (primitive) definition of Nat is

data Nat = Z | S Nat

We can match on:

• an arbitrary value using k
• the constructors. Here that's Z or S k . Of course S k would bind a different value to k than if we pattern matched on just k

Once you have matched on a value, you can do all the things you can normally do with a Nat, including constructing the successor using S, so if you wanted to match on S k and use it in a function, you could just

...
vectTake (S k) (x :: xs) = (S k) :: vectTake k xs

though here I've changed the meaning of your function to illustrate my point. In this example, you could also use a named pattern

...
vectTake count@(S k) (x :: xs) = count :: vectTake k xs

For your second question ...

By pred k I assume you mean predecessor not predicate. If so, you can do integer operations on Nat including k - 1, so, returning to the original definition of vecTake

...
vectTake k (x :: xs) = x :: vectTake (k - 1) xs

Note that this relies on the match for Z coming first, else you'll end up doing Z - 1 which won't compile.

As for which is better out of matching on Z and S k or Z and k, I can't think of any objective reason why one's better than the other. Perhaps performance comes into it in some cases but I can't help you there. I'd mostly use the constructor patterns cos people will be used to seeing that, but I'm sure there will be cases where other styles are warranted.