在 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_elemproof_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必须返回 a b，因此我们可以a与统一b。

Nowi也是auto，因此它不仅需要统一（这在这里没有帮助），而且此外，编译器还会查找“周围值”，如果没有指定明确的值，可以填补该漏洞。第一个查看我们没有的局部变量的地方是参数列表，我们确实在其中找到了j.

因此，我们对originresolve的调用无需显式指定任何其他参数。

你的情况更类似于这样：

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因此我们不能将其用作-parameterj的值。autoi

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