CODEWITHSUNDEEP
agda
ice1000
ice1000

Reputation: 6589

How to use type instances in Agda?

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?

Upvotes: 4

Views: 209

Answers (1)

gallais
gallais

Reputation: 12133

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
   (...)
   }

Upvotes: 2

Related Questions