'half' function type signature in Idris

4
votes

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.

2
dependent-typeidris

2 Answers

7
votes

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))

?

0
votes

You shouldn't use k twice. half : (n : Nat) -> (k : Nat) -> (n = k + k) -> Nat is correct, but useless. I think you need half : (n : Nat) -> Maybe (k ** n = k + k)