typeclass - 如何使用 Agda 标准库的类型类实例，例如也许是适用的？

Question

我对 Haskell 中的类型类、Idris 中的接口(interface)和 Scala 中的类型类模式都有经验；但是我还没有弄清楚如何使用Agda对类型类的编码或标准库中提供的类型类。 (我知道 Agda 中没有称为“类型类”的语言实体，但有多种其他功能组合在一起以允许对类型类进行编码，类似于 Scala。)

我有一个程序，我想在其中使用 Applicative 运算符；比如，对于 Maybe。当我尝试这样做时，我得到了一个模糊的类型错误；这是一个 MWE:

module Example where

open import Data.Bool
open import Category.Applicative using (RawApplicative)
open RawApplicative using (pure; _⊗_)
open import Data.Maybe.Categorical using (applicative)
open import Data.Maybe using (Maybe; nothing; just)

instance
  maybeApplicative = applicative

example : Maybe Bool
example = (nothing ⊗ just false) ⊗ just true

我得到的类型错误是:

Maybe _A_9 !=<Category.Applicative.Indexed.RawIApplicative (λ _ _ → _F_7)when checking that the expression nothing has typeRawApplicative _F_7

我如何在 Agda 中使用类型类中的函数/混合运算符？

Answer 1

instance maybeApplicative = applicative 声明(粗略地)当 ​​Agda 搜索类型为 RawApplicative {f} Maybe 的实例参数时，它应该使用 Data.Maybe .Categorical.applicative.

但是您的代码中没有任何内容会实际触发该实例搜索。实际上，如果您查看 _⊗_ 的类型，省略隐式参数，您会发现 (app : RawApplicative F) → F A → F B → F (A × B) ，因为您只是打开了一条记录。有两种相似的语法，您可能打算使用另一种:

open RawApplicative         using (pure; _⊗_) -- the one you used
-- _⊗_ : (app : RawApplicative F) → F A → F B → F (A × B)
open RawApplicative {{...}} using (pure; _⊗_) -- the one you meant to use
--                  ^^^^^^^
-- _⊗_ : {{app : RawApplicative F}} → F A → F B → F (A × B)
--       ^ notice this is now an instance argument

第二种语法打开记录，但在字段访问器中，记录参数将是一个实例参数(由 {{arg : ArgType}} 表示，与普通参数 (arg : ArgType) 和隐式参数 {arg : ArgType}) 和触发实例解析。

---

与您可能打算编写的内容无关 - 一旦您从上面进行更改，它应该编译

open import Data.Product
example : Maybe ((Bool × Bool) × Bool)
example = (nothing ⊗ just false) ⊗ just true

此外，作为 gallais在 reddit 上告诉我，在即将到来的 agda-stdlib v1.4 中，你可以导入 Data.Maybe.Instances对于您定义的实例。

---

另见 the relevant piece of documentation .