InstanceArguments

(redirected from ReferenceManual.Non-canonicalImplicitArguments)

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

TOC

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.