How to use the Agda standard library's typeclass instances, e.g. Maybe's Applicative?

Question

I have experience with type classes in Haskell, interfaces in Idris, and the typeclass pattern in Scala; but I have not figured out how to use Agda's encoding of typeclasses or the typeclasses provided in the standard library. (I am aware that there are not language entities called "typeclasses" in Agda but a variety of other features that combine to allow an encoding of type classes, similar to Scala.)

I have a program in which I want to use Applicative operators; say, for Maybe. I get an obscure type error when I try to do so; this is a 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

The type error I get is:

Maybe _A_9 !=< Category.Applicative.Indexed.RawIApplicative (λ _ _ → _F_7) when checking that the expression nothing has type RawApplicative _F_7

How do I make use of functions/mixfix operators from typeclasses in Agda?

WorldSEnder WorldSEnder · Accepted Answer · 2020-07-31T22:25:19

instance maybeApplicative = applicative declares (roughly) that when Agda searches for an instance argument of type RawApplicative {f} Maybe, it should use Data.Maybe.Categorical.applicative.

But nothing in your code actually triggers that instance search. Indeed, if you look at the type of _⊗_, omitting implicit arguments, you find (app : RawApplicative F) → F A → F B → F (A × B), because you simply opened a record. There are two similar syntaxes and you probably meant to use the other one:

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

The second syntax opens the record, but in the field accessors, the record argument will be an instance argument (denoted by {{arg : ArgType}} compared to normal arguments (arg : ArgType) and implicit arguments {arg : ArgType}) and trigger instance resolution.

Unrelated to that you probably meant to write - which should compile once you the change from above

open import Data.Product
example : Maybe ((Bool × Bool) × Bool)
example = (nothing ⊗ just false) ⊗ just true

Additionally, as gallais told me on reddit, in the upcoming v1.4 of the agda-stdlib, you can import Data.Maybe.Instances for the instance you defined.

See also the relevant piece of documentation.

How to use the Agda standard library's typeclass instances, e.g. Maybe's Applicative?

1 Answers