爲什麼涉及「mod」的平等不會在Idris中進行類型檢查？

v2 : 3 - 2 = 1 
v2 = Refl

2017-06-21 redfish64

它發生：

v1 : mod 3 2 = 1 
v1 = Refl

然而，這將類型檢查，罰款。它是多態的，默認數字常量是Integer s。

Idris> :t mod 
mod : Integral ty => ty -> ty -> ty 
Idris> :t 3 
3 : Integer 
Idris> :t mod 3 2 
mod 3 2 : Integer

對於Integermod類型的功能是不總。

取而代之的是使用modNatNZ函數，因此所有類型的檢測都是完美無缺的，並且工作正常。

v1 : modNatNZ 3 2 SIsNotZ = 1 
v1 = Refl

2017-06-21 12:21:49 Shersh

恐怕「在編譯器階段Idris只能在類型中執行模式匹配」這句話是不正確的。舉個例子，'（Int 3） - 2 = 1'，你可以用'Refl'來證明它，儘管'Int'不是一個歸納數據類型。正如你已經解釋過的，'Refl'不能用'mod'的原因是偏袒的。 –

回答