*(redirected from ReferenceManual.ModellingTypeClassesWithInstanceArguments)*

**See the official user manual for the most up-to-date version of the information on this page.**

Since version 2.3.0, Agda provides another type of implicit function arguments: instance arguments. The syntax and semantics for instance arguments was changed in Agda 2.4.2, and this manual only describes the new version.

### Syntax of instance arguments

An instance argument is defined similarly to an implicit function argument, except using double curly braces:

` ``f : {{x : A}} → B`

The double curly braces can also be replaced with the unicode
symbols `⦃`

and `⦄`

(type "\{{" and "\}}" in the Emacs Agda mode). This requires
spaces before and after the curly braces to make the Agda lexer notice
that they are not part of an identifier.

` ``f : ⦃ x : A ⦄ → B`

The syntax for instance arguments is analogous to that of Agda's normal implicit
arguments. Instance arguments can be explicitly supplied to a function, there exist
lambda expressions for them, you can use `forall`

syntax, and so on:

`f ⦃ x ⦄ = ...`

`λ ⦃ x : A ⦄ → e;`

`forall ⦃ x ⦄ -> ...`

### How instance arguments are resolved

Instance arguments differ from normal implicit arguments in one important aspect. Let's assume the following definitions are in scope.

`postulate A B : Set`

`f : ⦃ x : A ⦄ → B`

Then we can call `f`

without an explicit expression for argument `x`

,
and Agda will try to infer it.

`test : B`

`test = f`

However, instead of just inserting `_`

(like for normal implicit
arguments), Agda will look for *candidate expressions* in scope. A
candidate expression is any identifier (possibly applied to
hidden arguments) that is in scope, and that is one of the following:

- an identifier that has been declared with the special
`instance`

keyword; or - a constructor of a datatype or record; or
- a local variable (declared in a local
`let`

binding or as an argument of the current function).

During type-checking, Agda checks if only one such identifier has a correct type and using it as the implicit argument does not immediately invalidate other constraints. If so, this identifier is selected and used as the missing argument. For example, if we have

` ``instance postulate a : A`

as the only identifier of type `A`

in scope, then Agda will select it as
the missing identifier of the call to `f`

in the definition of `test`

above. Locally bound identifiers are also considered:

`test : A → B`

`test a = f`

or even

` ``test _ = f`

If two candiate identifiers are in scope:

` ``instance postulate a a' : A`

then Agda will not be able to solve the constraint, and the call to
`f`

will be marked in yellow in Emacs. If no valid identifier is in
scope, Agda will signal a type error.

Note: prior to Agda 2.4.2, there was no `instance`

keyword, and candidate expressions included *all* identifiers in scope. Starting from Agda 2.4.3, even datatype constructors will require an `instance`

keyword to become candidate expressions.

### A recursive example

Candidate identifiers may themselves depend on more instance arguments, in which case they will be resolved recursively.
For example, consider the following operation which extends any set `A`

by adding one more element `zero`

:

data Succ A : Set where zero : Succ A succ : A -> Succ A

We can inductively define a subtyping relation:

data _<:_ : Set -> Set -> Set₁ where base : {A : Set} -> A <: A step : {A B : Set} -> {{p : A <: B}} -> A <: Succ B

This allows us to define a canonical embedding of any subtype into its supertype:

cast : {A B : Set} -> {{p : A <: B}} -> A -> B cast {{base}} a = a cast {{step}} a = succ (cast a)

Since the argument `p`

to `cast`

and `step`

is an instance argument, Agda will attempt to resolve it automatically, using candidate expressions. For example:

plus3 : {A : Set} -> A -> Succ (Succ (Succ A)) plus3 x = cast x

Note that in resolving the instance argument `{{p}}`

to the `cast`

operator, the only candidate expressions Agda will consider are `base`

and `step`

. (Both of them are candiate expressions because they are datatype constructors). Since `step`

itself depends on an instance argument, it will be resolved recursively. In the above example, this succeeds uniquely, and the resulting term is equivalent to

plus3 x = cast {{step {{step {{step {{base}} }} }} }} x

Note: prior to Agda 2.4.2, instances were not resolved recursively.

### Using instance arguments to simulate Haskell type classes

Instance arguments can be used for different purposes, but they are
perhaps most useful as a replacement to Haskell type classes.
A typical example is Haskell's `Eq`

type class:

class Eq t where (==) :: t -> t -> Bool

We can model this in Agda using a record type:

record Eq (t : Set) : Set where field _==_ : t → t → Bool _/=_ : t → t → Bool a /= b = not $ a == b

We can now open a module containing versions of the `_==_`

and `_/=_`

functions taking the `Eq`

record as an instance
argument:

open Eq {{...}}

This brings in scope functions `_==_`

and `_/=_`

equivalent to the
following:

_==_ : {t : Set} → {{eqT : Eq t}} → t → t → Bool _==_ {{eqT}} = Eq._==_ eqT _/=_ : {t : Set} → {{eqT : Eq t}} → t → t → Bool _/=_ {{eqT}} = Eq._/=_ eqT

In fact, the syntax is equivalent to the following (except for not
defining the name `EqWithImplicits`

):

open module EqWithImplicits {t : Set} {{eqT : Eq t}} = Eq eqT

Now if we suppose that we have some instances of our "type class" in scope:

instance postulate eqℕ : Eq ℕ eqBool : Eq Bool

Then we can use the `_==_`

and `_/=_`

both on natural numbers and
booleans like their Haskell equivalents:

test = 5 == 3 ∧ true /= false

Note that `Eq`

is an ordinary Agda record. We can actually do the
same thing with any record from the standard library:

open import Relation.Binary using (IsDecEquivalence; module IsDecEquivalence; module DecSetoid) open import Data.Bool using (false; true; decSetoid) open DecSetoid decSetoid using (isDecEquivalence) open module IsDecEquivalenceWithImplicits {a ℓ} {A : Set a} {_≈_ : A → A → Set ℓ} {{ide : IsDecEquivalence _≈_}} = IsDecEquivalence ide test = false ≟ true

Note that the type of `test : false ≡ true`

is partially
defined by the value `isDecEquivalence`

that was selected for the
instance argument of the call to `_≟_`

. If a different
`isDecEquivalence`

was in scope, `test`

could have a different
value and also a different type.