让 Idris 相信递归调用的完整性

Question

我写了下面的类型来编码所有可能的有理数：

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number
    Ratio : Number -> Number -> Number

请注意 PosN Z 实际上编码数字 1，而 NegN Z 编码 -1。与 Data.ZZ 模块给出的定义相比，我更喜欢这样的对称定义。现在我有一个问题要说服 Idris，这样的数字相加是总数：

mul : Number -> Number -> Number
mul Zero _ = Zero
mul _ Zero = Zero
mul (PosN k) (PosN j) = PosN (S k * S j - 1)
mul (PosN k) (NegN j) = NegN (S k * S j - 1)
mul (NegN k) (PosN j) = NegN (S k * S j - 1)
mul (NegN k) (NegN j) = PosN (S k * S j - 1)
mul (Ratio a b) (Ratio c d) = Ratio (a `mul` b) (c `mul` d)
mul (Ratio a b) c = Ratio (a `mul` c) b
mul a (Ratio b c) = Ratio (a `mul` b) c

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = subtractNat k j
plus (NegN k) (PosN j) = subtractNat j k
plus (Ratio a b) (Ratio c d) =
    let a' = assert_smaller (Ratio a b) a in
    let b' = assert_smaller (Ratio a b) b in
    let c' = assert_smaller (Ratio c d) c in
    let d' = assert_smaller (Ratio c d) d in
    Ratio ((mul a' d') `plus` (mul b' c')) (mul b' d')
plus (Ratio a b) c =
    let a' = assert_smaller (Ratio a b) a in
    let b' = assert_smaller (Ratio a b) b in
    Ratio (a' `plus` (mul b' c)) c
plus a (Ratio b c) =
    let b' = assert_smaller (Ratio b c) b in
    let c' = assert_smaller (Ratio b c) c in
    Ratio ((mul a c') `plus` b') (mul a c')

有趣的是，当我在 Atom 编辑器中按下 Alt-Ctrl-R 时一切正常（即使使用 %default total 指令）。但是，当我将其加载到 REPL 中时，它会警告我 plus 可能不完整：

   |
29 |     plus Zero y = y
   |     ~~~~~~~~~~~~~~~
Data.Number.NumType.plus is possibly not total due to recursive path 
Data.Number.NumType.plus --> Data.Number.NumType.plus

从消息中我了解到它担心这些在模式处理比率中对 plus 的递归调用。我认为断言 a 小于 Ratio a b 等可以解决问题，但事实并非如此，所以 Idris 可能看到了这一点，但遇到了其他问题。不过我不知道它可能是什么。

Answer 1

assert_smaller (Ratio a b) a 已经为 Idris 所知（毕竟 a 是 "bigger" Ratio a b 类型的参数）。您需要证明（或断言）的是 mul 的结果在结构上小于 plus.

的参数

所以它应该适用于

plus (Ratio a b) (Ratio c d) =
    let x = assert_smaller (Ratio a b) (mul a d) in
    let y = assert_smaller (Ratio a b) (mul b c) in
    Ratio (x `plus` y) (mul b d)
plus (Ratio a b) c =
    let y = assert_smaller (Ratio a b) (mul b c) in
    Ratio (a `plus` y) c
plus a (Ratio b c) =
    let x = assert_smaller (Ratio b c) (mul a c) in
    Ratio (x `plus` b) (mul a c)

让 Idris 相信递归调用的完整性

Convince Idris about recursive call totality

idris

totality