recursion - Idris:尝试为 Nat 重新实现 fromInteger 时，完整性检查失败

Question

我有以下代码:

module Test
  data Nat' = S' Nat' | Z'
  Num Nat' where
    x * y = ?hole
    x + y = ?hole
    fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1))

我收到有关最后一行的错误消息:

Test.idr:6:5:
Prelude.Interfaces.Test.Nat' implementation of Prelude.Interfaces.Num, method fromInteger is
possibly not total due to recursive path Prelude.Interfaces.Test.Nat' implementation of
Prelude.Interfaces.Num, method fromInteger --> Prelude.Interfaces.Test.Nat' implementation of
Prelude.Interfaces.Num, method fromInteger

该函数应该始终给出结果，因为最终 fromInteger 的参数将变得足够小以选择第一种情况。但 idris 似乎并不明白这一点。这个函数有什么问题，如何修复这个错误？

Answer 1

n - 1结构上不小于n，要看到这一点，只需观察Integer不小于感应型。因此，您需要使用像 assert_smaller 这样的技巧让完整性检查器相信您的函数实际上是完整的(请参阅 Idris tutorial ):

这是它的current定义:

 assert_smaller : (x : a) -> (y : b) -> b
 assert_smaller x y = y

It simply evaluates to its second argument, but also asserts to the totality checker that y is structurally smaller than x.

这是 Idris 在其标准库中使用的内容(请参阅 here )来解决您的问题:

fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z