我对 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 type RawApplicative _F_7
我如何在 Agda 中使用类型类中的函数/混合运算符?
最佳答案
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
对于您定义的实例。
关于typeclass - 如何使用 Agda 标准库的类型类实例,例如也许是适用的?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/63198794/