如何在 Agda 中使用类型实例？

Question

我知道如何定义类型类，在阅读了 RawMonad、RawMonadZero、RawApplicative 等的定义后，我实现了一些简单的类型实例：

data Parser (A : Set) : Set where
  MkParser : (String → List (A × String)) → Parser A

ParserMonad : RawMonad Parser
ParserMonad = record {
    return = λ a → MkParser λ s → < a , s > ∷ []
  ; _>>=_  = λ p f → MkParser $ concatMap (tuple $ parse ∘ f) ∘ parse p
  }

但是当我试图在 ParserApplicative 的实现中使用 ParserMonad.return 时，我失败了：

ParserApplicative : RawApplicative Parser
ParserApplicative = record {
    pure = ParserMonad.return -- compile error
  ; _⊛_  = ...
  }

我的问题是：如何用ParserMonad.return实现ParserApplicative.pure？我该怎么做或者我应该阅读什么文档？

Answer 1

这里你没有使用实例参数，你使用的是记录。 Instance arguments 是一个独立的机制，结合记录，可以用来模拟类似类.

类型的东西

回到记录，要使用类型 R 的记录 r 的字段 f，您可以做各种事情：

使用应用于r的投影R.f：

 a = R.f r

将内容r对应的模块命名M为一个R并使用其中的定义f:

module M = R r
a = M.f

打开那个模块直接使用f:

open module R r
a = f

使用第一个替代方案，在你的情况下它会给我们：

ParserApplicative : RawApplicative Parser
ParserApplicative = record {
   pure = RawMonad.return ParserMonad
   (...)
   }

如何在 Agda 中使用类型实例？

How to use type instances in Agda?

agda