イドリス：全体のチェックが失敗したナット

Question

のために再実装fromIntegerしようとしたとき、私は次のコードを持っている：

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が、これはちょうどIntegerは誘導型ではないことを観察確認するために、nよりも構造的に小さいではありません。このように、あなたが実際に（イドリスtutorialを参照）assert_smallerのようなトリックを使用して合計され、あなたの関数チェッカ全体を説得する必要があります。

ここでは、そのcurrent定義です：

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

それは単にそのに評価しますyがxよりも構造的に小さいことをトータル・チェッカにアサートします。

これはあなたの問題のために（hereを参照）イドリスはその標準ライブラリに使用するものである：

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