使用命名实例来创建其他实例。

Question

我正在尝试在我的自定义Bool数据类型上，同时在运算符&&和||上创建Semigroup和VerifiedSemigroup实例：

%case data Lógico = Cierto | Falso

(&&) : Lógico -> Lógico -> Lógico
(&&) Cierto Cierto = Cierto
(&&) _ _ = Falso

(||) : Lógico -> Lógico -> Lógico
(||) Falso Falso = Falso
(||) _ _ = Cierto

因此，我首先为 && 运算符创建了一个命名实例，并使其成为 Semigroup 的一部分：

-- Todos
instance [TodosSemigroup] Semigroup Lógico where
    (<+>) a b = a && b

但是，在创建VerifiedSemigroup实例时，我如何告诉Idris使用Lógico的TodosSemigroup实例呢？

instance [TodosVerifiedSemigroup] VerifiedSemigroup Lógico where
    semigroupOpIsAssociative l c r = ?vsemigroupTodos

这段代码给我以下错误：

当推导 Prelude.Algebra.Main.TodosVerifiedSemigroup 的类型时， 方法 semigroupOpIsAssociative 发生了错误： 无法解析类型类 Semigroup Lógico

- chamini2

---

@dfeuer，我认为问题在于它没有被实现。 - chamini2

Answer 1

在idris-dev存储库中有一个未解决的问题。Edwin Brady表示：

“目前（按设计），命名实例只能通过显式命名来解析类，即使没有普通实例。”

因此，这里有Idris试图解析未命名的“Semigroup Lógico”实例，这是定义“VerifiedSemigroup Lógico”实例所需的。

我们需要一种方法，在实例声明中指定应使用命名实例来满足类约束。我不知道这是否可能。引用链接问题中的Edwin的话：

“这种行为没有任何文档记录”。

- Alexander Vieth

---

嗯，是的，我知道那就是问题所在。我需要知道的是如何告诉VerifiedSemigroup实例使用先前定义的Semigroup实例。 - chamini2

Answer 2

使用 using 关键字，引入了一个新的机制：

%case data Lógico = Cierto | Falso

(&&) : Lógico -> Lógico -> Lógico
(&&) Cierto Cierto = Cierto
(&&) _ _ = Falso

(||) : Lógico -> Lógico -> Lógico
(||) Falso Falso = Falso
(||) _ _ = Cierto

instance [TodosSemigroup] Semigroup Lógico where
    (<+>) a b = a && b

instance [TodosVerifiedSemigroup] VerifiedSemigroup Lógico using TodosSemigroup where
    semigroupOpIsAssociative l c r = ?vsemigroupTodos

- chamini2