Let's say we want to check the parity of an Int:
data Parity = Even | Odd
It would be pretty easy for Nat:
parity0: Nat -> Parity
parity0 Z = Even
parity0 (S k) = case parity0 k of
Even => Odd
Odd => Even
The first attempt to implement that for Int:
parity1: Int -> Parity
parity1 x = if mod x 2 == 0 then Even else Odd
This function is not total:
Main.parity1 is possibly not total due to: Prelude.Interfaces.Int implementation of Prelude.Interfaces.Integral
It makes sense because mod is not total for Int. (Although I'm not sure how I could know it in advance. The REPL shows that mod is total. Apparently, you can use a partial function to implement a total function of an interface? Strange.)
Next, I try to use DivBy view:
parity2: Int -> Parity
parity2 x with (divides x 2)
parity2 ((2 * div) + rem) | (DivBy prf) =
if rem == 0 then Even else Odd
This function works and is total, but the implementation is error-prone and doesn't scale to cases where we have multiple possible values. I'd like to assert that rem can only be 0 or 1. So I attempt to use case on rem:
parity3: Int -> Parity
parity3 x with (divides x 2)
parity3 ((2 * div) + rem) | (DivBy prf) = case rem of
0 => Even
1 => Odd
This function also works but is not total. How can I use prf provided by DivBy to convince the compiler that it's total? How can I use this prf in general?
Would using Integer or some other type make this problem easier to solve?
And there is another very concerning thing. I tried to case-split on prf and discovered that the following function is total:
parity4: Int -> Parity
parity4 x with (divides x 2)
parity4 ((2 * div) + rem) | (DivBy prf) impossible
Is that a bug? I can use this function to produce a runtime crash in a program that only contains total functions.