为什么在"伊德里斯"中不涉及"mod"的平等不是类型检查？

Question

为什么不会出现以下类型的问题:

v1 : mod 3 2 = 1
v1 = Refl

然而,这将很好地检查:

v2 : 3 - 2 = 1
v2 = Refl

Answer 1

这是由于mod功能的偏倚(感谢@AntonTrunov澄清).它是多态的,默认数字常量是Integers.

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

对于Integer类型mod功能不是全部.

而是使用modNatNZ功能,所以所有类型检查完美和工作.

v1 : modNatNZ 3 2 SIsNotZ = 1
v1 = Refl

我担心声明"在编译器阶段Idris只能在类型中执行模式匹配"是不对的.举例来说,`(Int 3) - 2 = 1`你可以使用`Refl`证明它,虽然`Int`不是归纳数据类型.正如你已经解释过的那样,`refl`与`mod`不兼容的原因是偏好. (3认同)