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.

An important difference between Haskell type classes and Agda’s instance arguments is that we use a non-recursive resolution for instance arguments