在 Idris 中定义组

Question

我在 Idris 中将幺半群定义为

interface Is_monoid (ty : Type) (op : ty -> ty -> ty) where
    id_elem : () -> ty
    proof_of_left_id : (a : ty) -> ((op a (id_elem ())) = a)
    proof_of_right_id : (a : ty) -> ((op (id_elem ())a) = a)
    proof_of_associativity : (a, b, c : ty) -> ((op a (op b c)) = (op (op a b) c)) 

然后尝试将组定义为

interface (Is_monoid ty op) => Is_group (ty : Type) (op : ty -> ty -> ty) where
    inverse : ty -> ty
    proof_of_left_inverse : (a : ty) -> (a = (id_elem ()))

但在编译过程中显示

When checking type of Group.proof_of_left_inverse:
Can't find implementation for Is_monoid ty op

有没有办法解决。

Answer 1

错误消息有点误导，但实际上，编译器不知道在proof_of_left_inverse 的定义中调用id_elem 时使用Is_monoid 的哪个实现。您可以通过使调用更明确来使其工作：

    proof_of_left_inverse : (a : ty) -> (a = (id_elem {ty = ty} {op = op} ()))

---

现在，为什么需要这样做？如果我们有一个简单的界面，比如

interface Pointed a where
  x : a

我们可以写一个类似的函数

origin : (Pointed b) => b
origin = x

没有明确指定任何类型参数。

理解这一点的一种方法是从其他方面来看待接口和实现，以一种更基本的 Idris 功能的方式。 x 可以认为是一个函数

x : {a : Type} -> {auto p : PointedImpl a} -> a

其中PointedImpl 是一些伪类型，代表Pointed 的实现。 （想想函数的记录。）

同样，origin 看起来像

origin : {b : Type} -> {auto j : PointedImpl b} -> b

x 特别有两个隐式参数，编译器会在类型检查和统一期间尝试推断。在上面的例子中，我们知道origin必须返回一个b，所以我们可以统一a和b。

现在i 也是auto，所以它不仅需要统一（这在这里没有帮助），而且如果没有明确的，编译器会寻找可以填补那个洞的“周围值”被指定。首先要查看我们没有的局部变量是参数列表，我们确实在其中找到了j。

因此，我们对origin 的调用可以解决，而无需我们显式指定任何其他参数。

你的情况更类似于这样：

interface Test a b where
  x : a
  y : b

test : (Test c d) => c
test = x

这会以与您的示例相同的方式出错。完成与上面相同的步骤，我们可以编写

x : {a : Type} -> {b -> Type} -> {auto i : TestImpl a b} -> a
test : {c : Type} -> {d -> Type} -> {auto j : TestImpl c d} -> c

如上所述，我们可以统一a 和c，但没有什么可以告诉我们d 应该是什么。具体来说，我们不能将它与b 统一，因此我们不能将TestImpl a b 与TestImpl c d 统一，因此我们不能将j 用作auto 参数i 的值。

---

请注意，我并没有声称这就是幕后实现的方式。从某种意义上说，这只是一个类比，但至少经得起一些审查。