Type of nonzero integers in Idris?

Question

I have a function that returns an integer that should be nonzero, and would like to guarantee that through its return type. How do you express the type of nonzero integers in Idris?

Answer 1

Depending on your function there are different ways. If you use Nat as return type, you could read about Theorem Proving in the Idris Tutorial. An example would be inc that increases a Nat and a proof incNotZ, that for every n : Nat, Not (inc n = Z):

inc : Nat -> Nat
inc n = S n

incNotZ : (n : Nat) -> Not (Z = inc n)
incNotZ n p = replace {P = incNotZTy} p ()
  where
    incNotZTy : Nat -> Type
    incNotZTy Z = ()
    incNotZTy (S k) = Void

Sometimes you can generate a proof alongside the result, f.e.:

data NotZero : Nat -> Type where
  MkNotZero : (n : Nat) -> NotZero (S n)

inc : (n : Nat) -> NotZero (S n)
inc n = MkNotZero n

rev : NotZero n -> Not (n = 0)
rev (MkNotZero n) = SIsNotZ -- from Prelude.Nat

Here NotZero n is a proof that n is not zero, as n can only be constructed via (S n). And indeed one can transform any NotZero n to Not (n = 0) with rev.

If your proof type fits the function this is often the better option. Because of both inc and NotZero having (n : Nat) -> … (S n) you get the proof for free. On the other hand, if you want to proof something about a function, what property it holds, like the commutativity or symmetry of plus, the first approach is needed.

---

If you are using Int as return type, this isn't usually useful, because Int can overflow and Idris can't argue about Int (or Integer or Float or …):

*main> 10000000000000000000 * (the Int 5)
-5340232221128654848 : Int

So the usual approach would be to construct a proof at runtime to see if the non-zeroness holds:

inc' : Int -> Int
inc' i = abs i + 1

incNotZ' : (i : Int) -> Either (So (inc' i == 0)) (So (not (inc' i == 0)))
incNotZ' i = choose (inc' i == 0)

Then when you call incNotZ' you can match on the result to get a proof on the right or handle the error case on the left.

If you are using for example non-overflowing Integer and are really, really sure that your function will never return a 0, you can force the compiler to believe you:

inc' : Integer -> Integer
inc' i = abs i + 1

incNotZ' : (i : Integer) -> Not (0 = inc' i)
incNotZ' i = believe_me