带有 Idris 接口的奇怪错误消息答案

【问题标题】：Strange error message with Idris interfaces带有 Idris 接口的奇怪错误消息
【发布时间】：2016-06-11 23:55:01
【问题描述】：

我正在尝试使用 Idris 接口实现一个简单的代数结构层次结构。代码如下：

module AlgebraicStructures

-- definition of some algebraic structures in terms of type classes

%access public export

Associative : {a : Type} -> (a -> a -> a) -> Type
Associative {a} op = (x : a) -> 
                     (y : a) ->
                     (z : a) ->
                     (op x (op y z)) = (op (op x y) z)

Identity : {a : Type} -> (a -> a -> a) -> a -> Type
Identity op v = ((x : a) -> (op x v) = x, 
                 (x : a) -> (op v x) = x)                 


Commutative : {a : Type} -> (a -> a -> a) -> Type
Commutative {a} op = (x : a) ->
                     (y : a) ->
                     (op x y) = (op y x)


infixl 4 <**>

interface IsMonoid a where
  empty  : a
  (<**>) : a -> a -> a 
  assoc  : Associative (<**>) 
  ident  : Identity (<**>) empty


interface IsMonoid a => IsCommutativeMonoid a where
  comm : Commutative (<**>)

但是，Idris 给出了这个奇怪的错误信息：

When checking type of constructor of AlgebraicStructures.IsCommutativeMonoid:
Can't find implementation for IsMonoid a

我相信 Idris 接口的工作方式类似于 Haskell 的类型类。在 Haskell 中，它应该可以工作。我在做傻事吗？

【问题讨论】：

标签： idris

【解决方案1】：

我相信它可能会抱怨，因为我不知道表达式 a 中有什么限制 Commutative (<**>) - 所以它不知道您可以在该类型上调用 <**>。显式指定 a 似乎对我有用 - Commutative {a} (<**>) - 我希望这意味着接口签名中的 a 在范围内并且可用于显式传递给其他类型。

【讨论】：