# Modelling Type Classes with Instance Arguments

Agda instance arguments can be used to model 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 a couple of “instances” of our “type class” in scope somehow:

`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`

Have you noticed 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.

As of version 2.4.2, instance search is also recursive (for definitions inside of `instance`

blocks), making it behave more like Haskell’s type classes. See the older page on non-recursive resolution for instance arguments for more about this.