typeclass - 将命名实例用于其他实例

Question

我正在尝试在 operator和 operator上对我的自定义数据类型Semigroup创建一个和VerifiedSemigroup实例：Bool&&||

%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

所以我首先为over 运算符创建一个命名实例：Semigroup&&

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

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

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

该代码给了我以下错误：

详细说明类型时Prelude.Algebra.Main.TodosVerifiedSemigroup，方法semigroupOpIsAssociative：无法解析类型类Semigroup Lógico

Answer 1

idris-dev 存储库中有一个未解决的问题。埃德温·布雷迪指出

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

所以这里我们让 Idris 尝试解析未命名的Semigroup Lógico实例，这是定义VerifiedSemigroup Lógico实例所必需的。

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

这种行为在任何地方都没有记录

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