Идрис: проверка целостности завершается неудачно при попытке повторно реализовать из Integer для Nat

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 станет достаточно маленьким, чтобы выбрать первый случай. Но Идрис, похоже, этого не понимает. Что не так с этой функцией, и как я могу исправить эту ошибку?

Answer 1

n - 1 конструктивно не меньше n, чтобы увидеть это просто понаблюдайте Integer не индуктивный тип. Таким образом, вам нужно убедить в проверке целостности, что ваша функция на самом деле полная, используя такой трюк, как assert_smaller (см. учебник Идрис):

Вот его текущее определение:

 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