无法消除名称歧义: Idris中的Prelude.List.++、Prelude.Strings.++错误

Question

目前，我正在尝试创建一个函数，它将Idris中的类型( ->，a -> a)作为参数，而正确的函数是idris中列表的++命令，不幸的是，我得到了这个错误。

ListMonoid：(A : Type) -> RawMonoid ListMonoid A= (A ** ([]，(++)

使用预期类型的ListMonoid检查RawMonoid的右手边时

无法消除名称的歧义: Prelude.List.++，Prelude.Strings.++

原始Monoid是下面的数据类型。

RawMonoid : RawMonoid = (M ** (M，M -> M -> M))内固定器6&

在我看来，它似乎不知道使用哪个++，有没有办法在调用中指定这一点？

Answer 1

您可以限定对(++)的引用，例如。

ListMonoid A = (A ** ([], List.(++)) )

还有一个with关键字，它以一个模块名作为它的第一个参数--它的基本意思是，“在下面的表达式中，先在这个模块中查找以解析名称”。

ListMonoid A = (A ** ([], with List (++)) )

但是，这两种方法都给出了代码中的以下类型错误：

    Type mismatch between
            List a -> List a -> List a (Type of (++))
    and
            A -> A -> A (Expected type)

如果我写：

ListMonoid A = (List A ** ([], (++)) )

它能够根据周围的类型约束选择正确的(++)。