Instance Arguments

TOC pl 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 curly braces can also be replaced with the following unicode symbols (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

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 ⦄ → e;

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 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 a hidden argument) 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 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

 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. Identifiers from the context are also considered:

 test : A → B
 test a = f

or even

 test _ = f

If two valid identifiers 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 identifier 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.