时间戳

首页 > 解决方案 > 如何使用 Agda 标准库的 typeclass 实例，例如 Maybe 的 Applicative？

typeclass - 如何使用 Agda 标准库的 typeclass 实例，例如 Maybe 的 Applicative？

问题描述

我有使用 Haskell 中的类型类、Idris 中的接口和 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

我得到的类型错误是：

可能 _A_9 !=< Category.Applicative.Indexed.RawIApplicative (λ _ _ → _F_7) 当检查表达式没有类型 RawApplicative _F_7

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

标签： typeclassagdaapplicativemaybe

解决方案

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 上告诉我的，在即将发布的 v1.4 的 agda-stdlib 中，您可以Data.Maybe.Instances为您定义的实例导入。

另请参阅相关文档。

推荐阅读