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

Question

我正在尝试制作 Semigroup和 VerifiedSemigroup我的自定义实例 Bool运算符 && 上的数据类型和运算符(operator) || :

%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 创建一个命名实例过&&运算符(operator):

-- 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

该代码给了我以下错误:

When elaborating type of Prelude.Algebra.Main.TodosVerifiedSemigroup, method semigroupOpIsAssociative: Can't resolve type class Semigroup Lógico

Answer 1

有一个open issue在 idris-dev 存储库中。埃德温布雷迪指出

Currently (by design) named instances can only be used to resolve a class by being named explicitly, even if there is no normal instance.

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

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

this behaviour isn't documented anywhere