Idris中的定义基团

Question

我在Idris中将monoid定义为

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

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

理解这一点的一种方法是通过其他透镜的角度看待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的值。

---

请注意，我并不是声称这是在幕后实施的方式。从某种意义上讲，这只是一个比喻，但至少要经过仔细的审查。