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.