Instance Arguments

TOC

Starting from Agda 2.3.0, Agda provides another type of implicit function arguments: instance arguments. These are defined as follows:

 f : {{x : A}} → B

The double accolades can also be replaced with the following unicode symbols (type “\{{” and “\}}” in the Emacs Agda mode). This requires spaces before and after the accolades to make the Agda lexer notice that they are not part of an identifier.

 f : ⦃ x : A ⦄ → B

Instance arguments behave very similar to Agda’s normal implicit arguments. They are defined in the same way:

 f : ⦃ x : A ⦄ → B
 f ⦃ x ⦄ = …

Lambda expressions exist for them:

 λ ⦃ x : A ⦄ → f ⦃ x ⦄

etc.

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 value 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 values in scope. A candidate value is any value in scope (either imported or defined previously in the file) or in the context (e.g. section arguments or arguments of the current function). During type-checking, Agda checks if only one such value has a correct type and using it as the implicit argument does not immediately invalidate other constraints. If so, this value is selected and used as the missing argument. For example, if we have

 postulate a : A

as the only value of type A in scope, then Agda will select it as the missing value of the call to f in the definition of test above. Values from the context are also considered:

 test : A → B
 test a = f

or even

 test _ = f

If two valid values are in scope:

 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 not a single value is in scope, Agda will signal a type error.

Instance arguments can be used for different purposes, but they are perhaps most useful as a replacement to Haskell type classes.