'half' function type signature in Idris

Question

I'm pretty new to Idris and I'm trying to catch the basic concepts and syntax.

Even if it may sound pointless, I'm trying to define a half function which is halving a natural.

I wish to come up with something like:

half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)

but of course it's not working. Specifically I get:

error: expected: dependent type signature

half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)

Is it possible?

Thanks.

Answer 1

What you want is to express that half n is some Natural number k such that n = k + k holds. The way to do it is by using a sigma type, i.e. a dependent pair of a number k and a proof n = k + k (it's a dependent pair because the type of the second coordinate, n = k + k depends on the value of the first coordinate, k).

The Idris standard library defines DPair for depedent pairs, including some syntax sugar allowing you to write

half : (n : Nat) -> (k ** n = k + k)

However, note that you won't be able to implement half (as a total function) because there's no good answer to e.g. half 1. Maybe what you want is

half : (n : Nat) -> (k ** Either (n = k + k) (n = k + k + 1))

?