How to use type instances in Agda?

Question

I know how to define typeclasses, and after reading the definition of RawMonad, RawMonadZero, RawApplicative and more, I implemented some simple type instances:

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
  }

But when I'm trying to use ParserMonad.return in the implementation of ParserApplicative, I failed:

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

My question is: how to use ParserMonad.return to implement ParserApplicative.pure? How can I do that or what doc should I read?

Please try to submit Minimal Complete and Verifiable Examples. Also, "I failed" is not very informative: if you got a compilation error, copy/paste it! — gallais

gallais gallais · Accepted Answer · 2017-11-20T21:47:09

Here you're not using instance arguments, you are using records. Instance arguments are an independent mechanism which, combined with records, can be used to simulate something like type classes.

Coming back to records, to use the field f of a record r of type R, you can do various things:

Use the projection R.f applied to r:

 a = R.f r

Name M the module corresponding to the content r as an R and use the definition f in it:

module M = R r
a = M.f

Open that module and use f directly:

open module R r
a = f

Using the first alternative, in your case it'd give us:

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

How to use type instances in Agda?

1 Answers