Download latest PDF - Read the Docs

Agda Documentation, Release 2.5
instance
ListMonoid : {a} {A : Set a} → Monoid (List A)
ListMonoid = record { mempty = []; _<>_ = _++_ }
Or equivalently, using copatterns:
instance
ListMonoid : {a} {A : Set a} → Monoid (List A)
mempty {{ListMonoid}} = []
_<>_
{{ListMonoid}} xs ys = xs ++ ys
Top-level instances must target a named type (Monoid in this case), and cannot be declared for types in the context.
Instances can have instance arguments themselves, which will be filled in recursively during instance resolution. For
instance,
record Eq {a} (A : Set a) : Set a where
field
_==_ : A → A → Bool
open Eq {{...}} public
instance
eqList : {a} {A : Set a} {{_ : Eq A}} → Eq (List A)
_==_ {{eqList}} []
[]
= true
_==_ {{eqList}} (x xs) (y ys) = x == y && xs == ys
_==_ {{eqList}} _
_
= false
eqNat : Eq Nat
_==_ {{eqNat}} = natEquals
ex : Bool
ex = (1 2
3
[]) == (1
2
[]) -- false
Note the two calls to _==_ in the right-hand side of the second clause. The first uses the Eq A instance and the second
uses a recursive call to eqList. In the example ex, instance resolution, needing a value of type Eq (List Nat),
will try to use the eqList instance and find that it needs an instance argument of type Eq Nat, it will then solve
that with eqNat and return the solution eqList {{eqNat}}.
Warning: At the moment there is no termination check on instances, so it is possible to make instance resolution loop by defining non-sensical instances like loop :
{a} {A : Set a} {{_ : Eq A}} →
Eq A.
Constructor instances
Although instance arguments are most commonly used for record types, mimicking Haskell-style type classes, they
can also be used with data types. In this case you often want the constructors to be instances, which is achieved by
declaring them inside an instance block. Typically arguments to constructors are not instance arguments, so during
instance resolution explicit arguments are treated as instance arguments. See instance resolution below for the details.
A simple example of a constructor that can be made an instance is the reflexivity constructor of the equality type:
data __ {a} {A : Set a} (x : A) : A → Set a where
instance refl : x x
This allows trivial equality proofs to be inferred by instance resolution, which can make working with functions that
have preconditions less of a burden. As an example, here is how one could use this to define a function that takes a
3.10. Instance Arguments
17