Classes

A class is a record that has several useful properties. A class is defined in the same way as a record, but it begins with the keyword \class instead of \record. Classes can extend other classes and records and vice versa. The first explicit parameter of a class is called its classifying field. Classes are implicitly coerced to the type of the classifying field. Let us consider an example:

\class Semigroup (E : \Set)
  | \infixl 7 * : E -> E -> E
  | *-assoc (x y z : E) : (x * y) * z = x * (y * z)

\func square {S : Semigroup} (x : S) => x * x

It is allowed to write x : S instead of x : S.E since S is implicitly coerced to an element of type \Set, that is S.E.

In case a parameter of a definition has type, which is an extension C { … } of C, it is marked as a local instance of class C. Implicit parameter \this of a field of class C is also a local instance.

If a parameter p : C { … } of a definition f is a local instance, then the corresponding implicit argument of f can be inferred by the instance inference algorithm. It looks for the first available instance v : C { … } such that the expected value of the classifying field coincides with the value of the classifying field in v. For instance, the function square in the example above has one local instance S of the class Semigroup. The field * of the class Semigroup is used in the body of square and the expected type of its call in x * x is S.E -> S.E -> {?}. This implies that the expected value of the classifying field is S.E, which coincides with the value of the classifying field in S, so this instance is inferred as the implicit argument of *.

Classifying fields

The classifying field can be specified explicitly with keyword \classifying as follows:

\class C (A : \Set) (\classifying B : \Set)
  | f : B -> A

\func test {c : C} (x : c) => f x

Since field B is marked as classifying, the type of x is c.B and the instance for f will be successfully inferred.

It is also possible to define a class without classifying fields. If the class has some explicit parameters, then this can be done using keyword \noclassifying, which is written after the name of the class.

Instances

It is also possible to define global instances. To do this, one needs to use the keyword \instance:

\instance NatSemigroup : Semigroup Nat
  | * => Nat.+
  | *-assoc (x y z : Nat) : (x Nat.+ y) Nat.+ z = x Nat.+ (y Nat.+ z) \elim z {
    | 0 => idp
    | suc z => pmap suc (*-assoc x y z)
  }

An implementation of a field can be defined by pattern matching as demonstrated above. In this case, a separate function with the same name as the field is created in the namespace of the instance.

A global instance is just a function, defined by copattern matching. It can be used as an ordinary function. The only difference with an ordinary function is that it can only be defined by copattern matching and must define an instance of a class. Also, the classifying field of an instance must be a data or a record applied to some arguments and if some parameters of the instance have a class as a type, its classifying field must be an argument of the classifying field of the resulting instance.

If there is no local instance with the expected classifying field, then such an instance will be searched among global instances. There is no backtracking, so the first appropriate instance will be chosen. A global instance is appropriate in a usage if the expected classifying field is the same data or record as the data or the record in the classifying field of the instance. If this holds, the global instance is appropriate even if the data or the record are applied to different arguments.