idris - 在 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

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

    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

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

理解这一点的一种方法是通过其他的镜头来看待接口(interface)和实现，以一种更基本的 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 .

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