Controlling Instance Search

An instance of the Add class is sufficient to allow two expressions with type Pos to be conveniently added, producing another Pos. However, in many cases, it can be useful to be more flexible and allow heterogeneous operator overloading, where the arguments may have different types. For example, adding a Nat to a Pos or a Pos to a Nat will always yield a Pos:

def addNatPos : Nat → Pos → Pos
  | 0, p => p
  | n + 1, p => Pos.succ (addNatPos n p)

def addPosNat : Pos → Nat → Pos
  | p, 0 => p
  | p, n + 1 => Pos.succ (addPosNat p n)

These functions allow natural numbers to be added to positive numbers, but they cannot be used with the Add type class, which expects both arguments to add to have the same type.

Heterogeneous Overloadings

As mentioned in the section on overloaded addition, Lean provides a type class called HAdd for overloading addition heterogeneously. The HAdd class takes three type parameters: the two argument types and the return type. Instances of HAdd Nat Pos Pos and HAdd Pos Nat Pos allow ordinary addition notation to be used to mix the types:

instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

instance : HAdd Pos Nat Pos where
  hAdd := addPosNat

Given the above two instances, the following examples work:

#eval (3 : Pos) + (5 : Nat)

8

#eval (3 : Nat) + (5 : Pos)

8

The definition of the HAdd type class is very much like the following definition of HPlus with the corresponding instances:

class HPlus (α : Type) (β : Type) (γ : Type) where
  hPlus : α → β → γ

instance : HPlus Nat Pos Pos where
  hPlus := addNatPos

instance : HPlus Pos Nat Pos where
  hPlus := addPosNat

However, instances of HPlus are significantly less useful than instances of HAdd. When attempting to use these instances with #eval, an error occurs:

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

typeclass instance problem is stuck, it is often due to metavariables
  HPlus Pos Nat ?m.7527

This happens because there is a metavariable in the type, and Lean has no way to solve it.

As discussed in the initial description of polymorphism, metavariables represent unknown parts of a program that could not be inferred. When an expression is written following #eval, Lean attempts to determine its type automatically. In this case, it could not. Because the third type parameter for HPlus was unknown, Lean couldn't carry out type class instance search, but instance search is the only way that Lean could determine the expression's type. That is, the HPlus Pos Nat Pos instance can only apply if the expression should have type Pos, but there's nothing in the program other than the instance itself to indicate that it should have this type.

One solution to the problem is to ensure that all three types are available by adding a type annotation to the whole expression:

#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos)

8

However, this solution is not very convenient for users of the positive number library.

Output Parameters

This problem can also be solved by declaring γ to be an output parameter. Most type class parameters are inputs to the search algorithm: they are used to select an instance. For example, in an OfNat instance, both the type and the natural number are used to select a particular interpretation of a natural number literal. However, in some cases, it can be convenient to start the search process even when some of the type parameters are not yet known, and use the instances that are discovered in the search to determine values for metavariables. The parameters that aren't needed to start instance search are outputs of the process, which is declared with the outParam modifier:

class HPlus (α : Type) (β : Type) (γ : outParam Type) where
  hPlus : α → β → γ

With this output parameter, type class instance search is able to select an instance without knowing γ in advance. For instance:

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

8

It might be helpful to think of output parameters as defining a kind of function. Any given instance of a type class that has one or more output parameters provides Lean with instructions for determining the outputs from the inputs. The process of searching for an instance, possibly recursively, ends up being more powerful than mere overloading. Output parameters can determine other types in the program, and instance search can assemble a collection of underlying instances into a program that has this type.

Default Instances

Deciding whether a parameter is an input or an output controls the circumstances under which Lean will initiate type class search. In particular, type class search does not occur until all inputs are known. However, in some cases, output parameters are not enough, and instance search should also occur when some inputs are unknown. This is a bit like default values for optional function arguments in Python or Kotlin, except default types are being selected.

Default instances are instances that are available for instance search even when not all their inputs are known. When one of these instances can be used, it will be used. This can cause programs to successfully type check, rather than failing with errors related to unknown types and metavariables. On the other hand, default instances can make instance selection less predictable. In particular, if an undesired default instance is selected, then an expression may have a different type than expected, which can cause confusing type errors to occur elsewhere in the program. Be selective about where default instances are used!

One example of where default instances can be useful is an instance of HPlus that can be derived from an Add instance. In other words, ordinary addition is a special case of heterogeneous addition in which all three types happen to be the same. This can be implemented using the following instance:

instance [Add α] : HPlus α α α where
  hPlus := Add.add

With this instance, hPlus can be used for any addable type, like Nat:

#eval HPlus.hPlus (3 : Nat) (5 : Nat)

8

However, this instance will only be used in situations where the types of both arguments are known. For example,

#check HPlus.hPlus (5 : Nat) (3 : Nat)

yields the type

HPlus.hPlus 5 3 : Nat

as expected, but

#check HPlus.hPlus (5 : Nat)

yields a type that contains two metavariables, one for the remaining argument and one for the return type:

HPlus.hPlus 5 : ?m.7706 → ?m.7708

In the vast majority of cases, when someone supplies one argument to addition, the other argument will have the same type. To make this instance into a default instance, apply the default_instance attribute:

@[default_instance]
instance [Add α] : HPlus α α α where
  hPlus := Add.add

With this default instance, the example has a more useful type:

#check HPlus.hPlus (5 : Nat)

yields

HPlus.hPlus 5 : Nat → Nat

Each operator that exists in overloadable heterogeneous and homogeneous versions follows the pattern of a default instance that allows the homogeneous version to be used in contexts where the heterogeneous is expected. The infix operator is replaced with a call to the heterogeneous version, and the homogeneous default instance is selected when possible.

Similarly, simply writing 5 gives a Nat rather than a type with a metavariable that is waiting for more information in order to select an OfNat instance. This is because the OfNat instance for Nat is a default instance.

Default instances can also be assigned priorities that affect which will be chosen in situations where more than one might apply. For more information on default instance priorities, please consult the Lean manual.

Exercises

Define an instance of HMul (PPoint α) α (PPoint α) that multiplies both projections by the scalar. It should work for any type α for which there is a Mul α instance. For example,

#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0

should yield

{ x := 5.000000, y := 7.400000 }