3

我有以下代码：

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 的参数将变得足够小以选择第一种情况。但伊德里斯似乎并不理解这一点。这个功能有什么问题，我该如何解决这个错误？

4

1 回答 1

4

n - 1在结构上不小于n，看到这只是观察到Integer不是归纳类型。因此，您需要使用类似的技巧来说服全数检查器您的函数实际上是全数的assert_smaller（请参阅 Idris教程）：

这是它当前的定义：

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

它只计算它的第二个参数，但也断言y结构上小于x.

这是 Idris 在其标准库中使用的（参见此处）解决您的问题：

fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z
于 2017-05-12T10:20:49.837 回答