如何在全函数中匹配整数范围？Int奇偶性实现疑难

咱们一步步拆解你遇到的Int奇偶性全函数实现问题，顺便理清那些让人困惑的细节：

1. 为什么parity1不是全函数？ #

你说得对，Idris的Int类型的mod并非全函数——这是因为Int是有界整数，当你对minBound（比如64位系统下的-2^63）执行mod 2时，会出现溢出，导致无法得到合法结果。而REPL显示mod是全函数，是因为Integral接口的签名是全函数，但具体到Int的实现是部分的，这确实有点反直觉，但Idris允许接口的实现是部分函数（虽然不推荐）。

2. 如何让parity3成为全函数？ #

DivBy视图返回的DivBy prf里包含了关键信息：余数rem满足0 ≤ rem < 2（也就是rem_lt : rem < 2）。我们可以利用这个证明，用absurd消除掉rem既不是0也不是1的不可能分支，让编译器认可这是全函数：

data Parity = Even | Odd

parity3 : Int -> Parity
parity3 x with (divides x 2)
parity3 ((2 * div) + rem) | (DivBy div rem x_eq rem_lt) = 
    case decEq rem 0 of
        Yes _ => Even
        No not_zero => case decEq rem 1 of
            Yes _ => Odd
            No not_one => absurd $ ltNotGe rem_lt not_one

这里的ltNotGe是Idris标准库的定理，用来证明如果a < b，那么a ≥ b是不可能的。因为rem < 2，而not_one证明了rem ≠ 1，结合not_zero的rem ≠ 0，就意味着rem ≥ 2，这和rem_lt矛盾，所以这个分支不可能存在，用absurd就能消除它。

3. 为什么parity4被认定为全函数？这是bug吗？ #

这不是bug，而是Idris视图匹配和impossible关键字的语义导致的：

• divides x 2对于任意Int x都是全的（因为除数2非零），所以with块只会进入DivBy分支，没有其他情况。
• impossible关键字告诉编译器："这个分支不可能被执行"，所以编译器认为函数没有遗漏分支，是全函数。但实际上，所有调用都会进入这个分支，运行时会触发impossible的崩溃错误。

这本质上是误用了impossible——它应该用来标记逻辑上不可能存在的分支，而这里的分支是必然存在的，所以运行时会出错。

4. 用Integer能否简化问题？ #

当然可以！Integer是无界整数，它的mod是全函数，所以直接用你最初的parity1风格就能写出全函数：

parityInteger : Integer -> Parity
parityInteger x = if mod x 2 == 0 then Even else Odd

如果你还是想用DivBy视图，Integer的divides同样能提供合法的余数证明，而且处理起来更直观，因为Integer的正负号逻辑不会干扰余数的范围（余数总是非负且小于除数）。

内容的提问来源于stack exchange，提问作者Pavel Strakhov