为什么在 Idris 中涉及“mod”的平等不进行类型检查？答案

【问题标题】：Why doesn't equality involving "mod" not typecheck in Idris?为什么在 Idris 中涉及“mod”的平等不进行类型检查？
【发布时间】：2017-11-24 03:36:57
【问题描述】：

为什么不进行以下类型检查：

v1 : mod 3 2 = 1
v1 = Refl

但这会很好地进行类型检查：

v2 : 3 - 2 = 1
v2 = Refl

【问题讨论】：

【解决方案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 只能在类型中执行模式匹配”的说法是不正确的。以(the Int 3) - 2 = 1 为例，您可以使用Refl 来证明它，尽管Int 不是归纳数据类型。 Refl 不适用于 mod 的原因是偏心，正如您已经解释的那样。