An operation is polymorphic if it can be used with multiple types.
In Lean, polymorphism comes in three varieties:
universe polymorphism, where the sorts in a definition can be instantiated in various ways,
functions that take types as (potentially implicit) parameters, allowing a single body of code to work with any type, and
ad-hoc polymorphism, implemented with type classes, in which operations to be overloaded may have different implementations for different types.
Because Lean does not allow case analysis of types, polymorphic functions implement operations that are uniform for any choice of type argument; for example, List.map does not suddenly compute differently depending on whether the input list contains Strings or Nats.
Ad-hoc polymorphic operations are useful when there is no “uniform” way to implement an operation; the canonical use case is for overloading arithmetic operators so that they work with Nat, Int, Float, and any other type that has a sensible notion of addition.
Ad-hoc polymorphism may also involve multiple types; looking up a value at a given index in a collection involves the collection type, the index type, and the type of member elements to be extracted.
A type classType classes were first described in Philip Wadler and Stephen Blott, 1980. “How to make ad-hoc polymorphism less ad hoc”. In Proceedings of the 16th Symposium on Principles of Programming Languages. describes a collection of overloaded operations (called methods) together with the involved types.
Type classes are very flexible.
Overloading may involve multiple types; operations like indexing into a data structure can be overloaded for a specific choice of data structure, index type, element type, and even a predicate that asserts the presence of the key in the structure.
Due to Lean's expressive type system, overloading operations is not restricted only to types; type classes may be parameterized by ordinary values, by families of types, and even by predicates or propositions.
All of these possibilities are used in practice:
Natural number literals
The OfNat type class is used to interpret natural number literals.
Instances may depend not only on the type being instantiated, but also on the number literal itself.
Computational effects
Type classes such as Monad, whose parameter is a function from one type to another, are used to provide special syntax for effectful operations.
The “type” for which operations are overloaded is actually a type-level function, such as Option, IO, or Except.
Predicates and propositions
The Decidable type class allows a decision procedure for a proposition to be found automatically by Lean.
This is used as the basis for termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
if-expressions, which may branch on any decidable proposition.
While ordinary polymorphic definitions simply expect instantiation with arbitrary parameters, the operators overloaded with type classes are to be instantiated with instances that define the overloaded operation for some specific set of parameters.
These instance-implicit parameters are indicated in square brackets.
At invocation sites, Lean either synthesizes a suitable instance from the available candidates or signals an error.
Because instances may themselves have instance parameters, this search process may be recursive and result in a final composite instance value that combines code from a variety of instances.
Thus, type class instance synthesis is also a means of constructing programs in a type-directed manner.
Here are some typical use cases for type classes:
Type classes may represent overloaded operators, such as arithmetic that can be used with a variety of types of numbers or a membership predicate that can be used for a variety of data structures. There is often a single canonical choice of operator for a given type—after all, there is no sensible alternative definition of addition for Nat—but this is not an essential property, and libraries may provide alternative instances if needed.
Type classes can represent an algebraic structure, providing both the extra structure and the axioms required by the structure. For example, a type class that represents an Abelian group may contain methods for a binary operator, a unary inverse operator, an identity element, as well as proofs that the binary operator is associative and commutative, that the identity is an identity, and that the inverse operator yields the identity element on both sides of the operator. Here, there may not be a canonical choice of structure, and a library may provide many ways to instantiate a given set of axioms; there are two equally canonical monoid structures over the integers.
A type class can represent a relation between two types that allows them to be used together in some novel way by a library.
The Coe class represents automatically-inserted coercions from one type to another, and MonadLift represents a way to run operations with one kind of effect in a context that expects another kind.
Type classes can represent a framework of type-driven code generation, where instances for polymorphic types each contribute some portion of a final program.
The Repr class defines a canonical pretty-printer for a datatype, and polymorphic types end up with polymorphic Repr instances.
When pretty printing is finally invoked on an expression with a known concrete type, such as List(Nat×(String⊕Int)), the resulting pretty printer contains code assembled from the Repr instances for List, Prod, Nat, Sum, String, and Int.
The Lean.Parser.Command.declaration : commandclass declaration creates a new single-constructor inductive type, just as if the Lean.Parser.Command.declaration : commandstructure command had been used instead.
In fact, the results of the Lean.Parser.Command.declaration : commandclass and Lean.Parser.Command.declaration : commandstructure commands are almost identical, and features such as default values may be used the same way in both.
Please refer to the documentation for structures for more information about default values, inheritance, and other features of structures.
The differences between structure and class declarations are:
Methods instead of fields
Instead of creating field projections that take a value of the structure type as an explicit parameter, methods are created. Each method takes the corresponding instance as an instance-implicit parameter.
Instance-implicit parent classes
The constructor of a class that extends other classes takes its class parents' instances as instance-implicit parameters, rather than explicit parameters.
When instances of this class are defined, instance synthesis is used to find the values of inherited fields.
Parents that are not classes are still explicit parameters to the underlying constructor.
Parent projections via instance synthesis
Structure field projections make use of inheritance information to project parent structure fields from child structure values.
Classes instead use instance synthesis: given a child class instance, synthesis will construct the parent; thus, methods are not added to child classes in the same way that projections are added to child structures.
Registered as class
The resulting datatype is registered as a type class, for which instances may be defined and that may be used as the type of instance-implicit arguments.
Out and semi-out parameters are considered
The outParam and semiOutParamgadgets have no meaning in structure definitions, but they are used in class definitions to control instance search.
While Lean.Parser.Command.declaration : commandderiving clauses are allowed for class definitions to maintain the parallel between class and structure elaboration, they are not frequently used and should be considered an advanced feature.
No Instances of Non-Classes
Lean rejects instance-implicit parameters of types that are not classes:
deff[n:invalid binder annotation, type is not a class instance
Nat
use the command `set_option checkBinderAnnotations false` to disable the checkNat]:n=n:=rfl
invalid binder annotation, type is not a class instance
Nat
use the command `set_option checkBinderAnnotations false` to disable the check
Class vs Structure Constructors
A very small algebraic hierarchy can be represented either as structures (S.Magma, S.Semigroup, and S.Monoid below), a mix of structures and classes (C1.Monoid), or only using classes (C2.Magma, C2.Semigroup, and C2.Monoid):
Finally, C2.Monoid.mk takes its semigroup parent as an instance implicit parameter.
The references to op become references to the method C2.Magma.op, relying on instance synthesis to recover the implementation from the C2.Semigroup instance-implicit parameter via its parent projection:
Parameters to type classes may be marked with gadgets, which are special versions of the identity function that cause the elaborator to treat a value differently.
Gadgets never change the meaning of a term, but they may cause it to be treated differently in elaboration-time search procedures.
The gadgets outParam and semiOutParam affect instance synthesis, so they are documented in that section.
Whether a type is a class or not has no effect on definitional equality.
Two instances of the same class with the same parameters are not necessarily identical and may in fact be very different.
Instances are Not Unique
This implementation of binary heap insertion is buggy:
In the improved definitions, Heap'.bubbleUp is needlessly explicit; the instance does not need to be explicitly named here because Lean would select the indicated instances nonetheless, but it does bring the correctness invariant front and center for readers.
Most type classes follow the paradigm of a set of overloaded methods from which clients may choose freely.
This is naturally modeled by a product type, from which the overloaded methods are projections.
Some classes, however, are sum types: they require that the recipient of the synthesized instance first check which of the available instance constructors was provided.
To account for these classes, a class declaration may consist of an arbitrary inductive type, not just an extended form of structure declaration.
Class inductive types are just like other inductive types, except they may participate in instance synthesis.
The paradigmatic example of a class inductive is Decidable: synthesizing an instance in a context with free variables amounts to synthesizing the decision procedure, but if there are no free variables, then the truth of the proposition can be established by instance synthesis alone (as is done by the decide tactic).
In some cases, many related type classes may co-occur throughout a codebase.
Rather than writing all the names repeatedly, it would be possible to define a class that extends all the classes in question, contributing no new methods itself.
However, this new class has a disadvantage: its instances must be declared explicitly.
The Lean.Parser.Command.classAbbrev : commandExpands
```
class abbrev C <params> := D_1, ..., D_n
```
into
```
class C <params> extends D_1, ..., D_n
attribute [instance] C.mk
```
class abbrev command allows the creation of class abbreviations in which one name is short for a number of other class parameters.
Behind the scenes, a class abbreviation is represented by a class that extends all the others.
Its constructor is additionally declared to be an instance so the new class can be constructed by instance synthesis alone.
Class Abbreviations
Both plusTimes1 and plusTimes2 require that their parameters' type have Add and Mul instances:
Because AddMul is a Lean.Parser.Command.classAbbrev : commandExpands
```
class abbrev C <params> := D_1, ..., D_n
```
into
```
class C <params> extends D_1, ..., D_n
attribute [instance] C.mk
```
class abbrev, no additional declarations are necessary to use plusTimes1 with Nat:
37#evalplusTimes1257
37
However, plusTimes2 fails, because there is no AddMul'Nat instance—no instances whatsoever have yet been declared:
#evalfailed to synthesize
AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.plusTimes2257
failed to synthesize
AddMul' ?m.22
Additional diagnostic information may be available using the `set_option diagnostics true` command.
Declaring an very general instance takes care of the problem for Nat and every other type:
The syntax of instance declarations is almost identical to that of definitions.
The only syntactic differences are that the keyword Lean.Parser.Command.declaration : commanddef is replaced by Lean.Parser.Command.declaration : commandinstance and the name is optional:
syntax
Most instances define each method using Lean.Parser.Command.declaration : commandwhere syntax:
instance::= ...
|`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance((priority:=prio))?`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId?`declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSigwhere(whereStructField),*
However, type classes are inductive types, so instances can be constructed using any expression with an appropriate type:
instance::= ...
|`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance((priority:=prio))?`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId?`declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig:=termTermination hints are `termination_by` and `decreasing_by`, in that order.
Instances may also be defined by cases; however, this feature is rarely used outside of Decidable instances:
instance::= ...
|`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. instance((priority:=prio))?`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId?`declSig` matches the signature of a declaration with required type: a list of binders and then `: type` declSig(|term=>term)*Termination hints are `termination_by` and `decreasing_by`, in that order.
Instances defined with explicit terms often consist of either anonymous constructors (Lean.Parser.Term.anonymousCtor : termThe *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
expected type is an inductive type with a single constructor `c`.
If more terms are given than `c` has parameters, the remaining arguments
are turned into a new anonymous constructor application. For example,
`⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
⟨...⟩) wrapping method implementations or of invocations of inferInstanceAs on definitionally equal types.
Elaboration of instances is almost identical to the elaboration of ordinary definitions, with the exception of the caveats documented below.
If no name is provided, then one is created automatically.
It is possible to refer to this generated name directly, but the algorithm used to generate the names has changed in the past and may change in the future.
It's better to explicitly name instances that will be referred to directly.
After elaboration, the new instance is registered as a candidate for instance search.
Adding the attribute instance to a name can be used to mark any other defined name as a candidate.
Functions defined in Lean.Parser.Command.declaration : commandwhere structure definition syntax are not recursive.
Because instance declaration is a version of structure definition, type class methods are also not recursive by default.
Instances for recursive inductive types are common, however.
There is a standard idiom to work around this limitation: define a recursive function independently of the instance, and then refer to it in the instance definition.
By convention, these recursive functions have the name of the corresponding method, but are defined in the datatype's namespace.
instance:BEqNatTreewherebeq|.leaf,.leaf=>true|.branchl1v1r1,.branchl2v2r2=>failed to synthesize
BEq NatTree
Additional diagnostic information may be available using the `set_option diagnostics true` command.l1==l2&&v1==v2&&failed to synthesize
BEq NatTree
Additional diagnostic information may be available using the `set_option diagnostics true` command.r1==r2|_,_=>false
with errors in both the left and right recursive calls that read:
failed to synthesize
BEq NatTree
Additional diagnostic information may be available using the `set_option diagnostics true` command.
Given a suitable recursive function, such as NatTree.beq:
or, equivalently, using anonymous constructor syntax:
instance:BEqNatTree:=⟨NatTree.beq⟩
Furthermore, instances are not available for instance synthesis during their own definitions.
They are first marked as being available for instance synthesis after they are defined.
Nested inductive types, in which the recursive occurrence of the type occurs as a parameter to some other inductive type, may require an instance to be available to write even the recursive function.
The standard idiom to work around this limitation is to create a local instance in a recursively-defined function that includes a reference to the function being defined, taking advantage of the fact that instance synthesis may use every binding in the local context with the right type.
Instances for nested types
In this definition of NatRoseTree, the type being defined occurs nested under another inductive type constructor (Array):
Checking the equality of rose trees requires checking equality of of arrays.
However, instances are not typically available for instance synthesis during their own definitions, so the following definition fails, even though NatRoseTree.beq is a recursive function and is in scope in its own definition.
defNatRoseTree.beq:(tree1tree2:NatRoseTree)→Bool|.nodeval1children1,.nodeval2children2=>val1==val2&&failed to synthesize
BEq (Array NatRoseTree)
Additional diagnostic information may be available using the `set_option diagnostics true` command.children1==children2
failed to synthesize
BEq (Array NatRoseTree)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
To solve this, a local BEqNatRoseTree instance may be let-bound:
Many instances have function types: any instance that itself recursively invokes instance search is a function, as is any instance with implicit parameters.
While most instances only project method implementations from their own instance parameters, instances of class inductives typically pattern-match one or more of their arguments, allowing the instance to select the appropriate constructor.
This is done using ordinary Lean function syntax.
Just as with other instances, the function in question is not available for instance synthesis in its own definition.
An instance for a sum class
Because DecidableEqα is an abbreviation for (ab:α)→Decidable(Eqab), its arguments can be used directly, as in this example:
inductiveThreeChoiceswhere|yes|no|maybeinstance:DecidableEqThreeChoices|.yes,.yes=>.isTruerfl|.no,.no=>.isTruerfl|.maybe,.maybe=>.isTruerfl|.yes,.maybe|.yes,.no|.maybe,.yes|.maybe,.no|.no,.yes|.no,.maybe=>.isFalsenofunA recursive instance for a sum class
The type StringList represents monomorphic lists of strings:
In the following attempt at defining a DecidableEq instance, instance synthesis invoked while elaborating the inner termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
if fails because the instance is not available for instance synthesis in its own definition:
instance:DecidableEqStringList|.nil,.nil=>.isTruerfl|.consh1t1,.consh2t2=>ifh:h1=h2thenfailed to synthesize
Decidable (t1 = t2)
Additional diagnostic information may be available using the `set_option diagnostics true` command.ifh':t1=t2then.isTrue(h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':t1 = t2⊢ StringList.consh1t1 = StringList.consh2t2All goals completed! 🐙)else.isFalse(h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬t1 = t2⊢ ¬StringList.consh1t1 = StringList.consh2t2h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬t1 = t2hEq:StringList.consh1t1 = StringList.consh2t2⊢ False;h1:Stringt1:StringListh:h1 = h1h':¬t1 = t1⊢ False;All goals completed! 🐙)else.isFalse(h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2⊢ ¬StringList.consh1t1 = StringList.consh2t2h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2hEq:StringList.consh1t1 = StringList.consh2t2⊢ False;h1:Stringt1:StringListh:¬h1 = h1⊢ False;All goals completed! 🐙)|.nil,.cons__|.cons__,.nil=>.isFalsenofun
failed to synthesize
Decidable (t1 = t2)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
However, because it is an ordinary Lean function, it can recursively refer to its own explicitly-provided name:
instanceinstDecidableEqStringList:DecidableEqStringList|.nil,.nil=>.isTruerfl|.consh1t1,.consh2t2=>ifh:h1=h2thenifh':application type mismatch
@dite ?m.74 (instDecidableEqStringList t1 t2)
argument
instDecidableEqStringList t1 t2
has type
Decidable (t1 = t2) : Type
but is expected to have type
Prop : TypeinstDecidableEqStringListt1t2then.isTrue(h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':sorry⊢ StringList.consh1t1 = StringList.consh2t2h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':sorry⊢ t1 = t2)else.isFalse(h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬sorry⊢ ¬StringList.consh1t1 = StringList.consh2t2h1:Stringt1:StringListh2:Stringt2:StringListh:h1 = h2h':¬sorryhEq:StringList.consh1t1 = StringList.consh2t2⊢ False;h1:Stringt1:StringListh':¬sorryh:h1 = h1⊢ False;h1:Stringt1:StringListh':¬sorryh:h1 = h1⊢ False)else.isFalse(h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2⊢ ¬StringList.consh1t1 = StringList.consh2t2h1:Stringt1:StringListh2:Stringt2:StringListh:¬h1 = h2hEq:StringList.consh1t1 = StringList.consh2t2⊢ False;h1:Stringt1:StringListh:¬h1 = h1⊢ False;All goals completed! 🐙)|.nil,.cons__|.cons__,.nil=>.isFalsenofun
Instances may be assigned priorities.
During instance synthesis, higher-priority instances are preferred; see the section on instance synthesis for details of instance synthesis.
If no priority is specified, the default priority that corresponds to 1000 is used:
prio::= ...
|The default priority `default = 1000`, which is used when no priority is set. default
Three named priorities are available when numeric values are too fine-grained, corresponding to 100, 500, and 10000 respectively.
The prioMid : prioThe standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`.
mid priority is lower than prioDefault : prioThe default priority `default = 1000`, which is used when no priority is set. default.
prio::= ...
|The standardized "low" priority `low = 100`, for things that should be lower than default priority. low
prio::= ...
|The standardized "medium" priority `mid = 500`. This is lower than `default`, and higher than `low`.
mid
prio::= ...
|The standardized "high" priority `high = 10000`, for things that should be higher than default priority. high
Finally, priorities can be added and subtracted, so default + 2 is a valid priority, corresponding to 1002:
prio::= ...
|Parentheses are used for grouping priority expressions. (prio)
prio::= ...
|Addition of priorities. This is normally used only for offsetting, e.g. `default + 1`. prio+prio
prio::= ...
|Subtraction of priorities. This is normally used only for offsetting, e.g. `default - 1`. prio-prio
A default instance of OfNatNat is used to select Nat for natural number literals in the absence of other type information.
It is declared in the Lean standard library with priority 100.
Given this representation of even numbers, in which an even number is represented by half of it:
structureEvenwherehalf:Nat
the following instances allow numeric literals to be used for small Even values (a limit on the depth of type class instance search prevents them from being used for arbitrarily large literals):
The instance attribute declares a name to be an instance, with the specified priority.
Like other attributes, instance can be applied globally, locally, or only when the current namespace is opened.
The Lean.Parser.Command.declaration : commandinstance declaration is a form of definition that automatically applies the instance attribute.
syntax
Declares the definition to which it is applied to be an instance.
If no priority is provided, then the default priority default is used.
Instance synthesis is a recursive search procedure that either finds an instance for a given type class or fails.
In other words, given a type that is registered as a type class, instance synthesis attempts constructs a term with said type.
It respects reducibility: semireducible or irreducible definitions are not unfolded, so instances for a definition are not automatically treated as instances for its unfolding unless it is reducible.
There may be multiple possible instances for a given class; in this case, declared priorities and order of declaration are used as tiebreakers, in that order, with more recent instances taking precedence over earlier ones with the same priority.
This search procedure is efficient in the presence of diamonds and does not loop indefinitely when there are cycles.
Diamonds occur when there is more than one route to a given goal, and cycles are situations when two instances each could be solved if the other were solved.
Diamonds occur regularly in practice when encoding mathematical concepts using type classes, and Lean's coercion feature naturally leads to cycles, e.g. between finite sets and finite multisets.
Instance synthesis can be tested using the Lean.Parser.Command.synth : command#synth command.
syntax
The Lean.Parser.Command.synth : command#synth command attempts to synthesize an instance for the provided class.
If it succeeds, then the resulting term is output.
command::= ...
|#synthterm
Additionally, inferInstance and inferInstanceAs can be used to synthesize an instance in a position where the instance itself is needed.
inferInstance synthesizes a value of any target type by typeclass
inference. This function has the same type signature as the identity
function, but the square brackets on the [i : α] argument means that it will
attempt to construct this argument by typeclass inference. (This will fail if
α is not a class.) Example:
inferInstanceAs α synthesizes a value of any target type by typeclass
inference. This is just like inferInstance except that α is given
explicitly instead of being inferred from the target type. It is especially
useful when the target type is some α' which is definitionally equal to α,
but the instance we are looking for is only registered for α (because
typeclass search does not unfold most definitions, but definitional equality
does.) Example:
Generally speaking, instance synthesis is a recursive search procedure that may, in general, backtrack arbitrarily.
Synthesis may succeed with an instance term, fail if no such term can be found, or get stuck if there is insufficient information.
A detailed description of the instance synthesis algorithm is available in Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura (2020)Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura, 2020. “Tabled typeclass resolution”. arXiv:2001.04301.
An instance search problem is given by a type class applied to concrete arguments; these argument values may or may not be known.
Instance search attempts every locally-bound variable whose type is a class, as well as each registered instance, in order of priority and definition.
When candidate instances themselves have instance-implicit parameters, they impose further synthesis tasks.
A problem is only attempted when all of the input parameters to the type class are known.
When a problem cannot yet be attempted, then that branch is stuck; progress in other subproblems may result in the problem becoming solvable.
Output or semi-output parameters may be either known or unknown at the start of instance search.
Output parameters are ignored when checking whether an instance matches the problem, while semi-output parameters are considered.
Every candidate solution for a given problem is saved in a table; this prevents infinite regress in case of cycles as well as exponential search overheads in the presence of diamonds (that is, multiple paths by which the same goal can be achieved).
A branch of the search fails when any of the following occur:
All potential instances have been attempted, and the search space is exhausted.
The instance size limit specified by the option synthInstance.maxSize is reached.
The synthesized value of an output parameter does not match the specified value in the search problem.
Failed branches are not retried.
If search would otherwise fail or get stuck, the search process attempts to use matching default instances in order of priority.
For default instances, the input parameters do not need to be fully known, and may be instantiated by the instances parameter values.
Default instances may take instance-implicit parameters, which induce further recursive search.
Successful branches in which the problem is fully known (that is, in which there are no unsolved metavariables) are pruned, and further potentially-successful instances are not attempted, because no later instance could cause the previously-succeeding branch to fail.
3.6.3.2. Instance Search Problems
Instance search occurs during the elaboration of (potentially nullary) function applications.
Some of the implicit parameters' values are forced by others; for instance, an implicit type parameter may be solved using the type of a later value argument that is explicitly provided.
Implicit parameters may also be solved using information from the expected type at that point in the program.
The search for instance implicit arguments may make use of the implicit argument values that have been found, and may additionally solve others.
Instance synthesis begins with the type of the instance-implicit parameter.
This type must be the application of a type class to zero or more arguments; these argument values may be known or unknown when search begins.
If an argument to a class is unknown, the search process will not instantiate it unless the corresponding parameter is marked as an output parameter, explicitly making it an output of the instance synthesis routine.
Search may succeed, fail, or get stuck; a stuck search may occur when an unknown argument value becoming known might enable progress to be made.
Stuck searches may be re-invoked when the elaborator has discovered one of the previously-unknown implicit arguments.
If this does not occur, stuck searches become failures.
3.6.3.3. Candidate Instances
Instance synthesis uses both local and global instances in its search.
Local instances are those available in the local context; they may be either parameters to a function or locally defined with let.
Local instances do not need to be indicated specially; any local variable whose type is a type class is a candidate for instance synthesis.
Global instances are those available in the global environment; every global instance is a defined name with the instance attribute applied.Lean.Parser.Command.declaration : commandinstance declarations automatically apply the instance attribute.
Local Instances
In this example, addPairs contains a locally-defined instance of AddNatPair:
The search process for instances is largely governed by class parameters.
Type classes take a certain number of parameters, and instances are tried during the search when their choice of parameters is compatible with those in the class type for which the instance is being synthesized.
Instances themselves may also take parameters, but the role of instances' parameters in instance synthesis is very different.
Instances' parameters represent either variables that may be instantiated by instance synthesis or further synthesis work to be done before the instance can be used.
In particular, parameters to instances may be explicit, implicit, or instance-implicit.
If they are instance implicit, then they induce further recursive instance searching, while explicit or implicit parameters must be solved by unification.
Implicit and Explicit Parameters to Instances
While instances typically take parameters either implicitly or instance-implicitly, explicit parameters may be filled out as if they were implicit during instance synthesis.
In this example, aNonemptySumInstance is found by synthesis, applied explicitly to Nat, which is needed to make it type-correct.
In the output, both the explicit argument Nat and the implicit argument Empty were found by unification with the search goal, while the NonemptyNat instance was found via recursive instance synthesis.
By default, the parameters of a type class are considered to be inputs to the search process.
If the parameters are not known, then the search process gets stuck, because choosing an instance would require the parameters to have values that match those in the instance, which cannot be determined on the basis of incomplete information.
In most cases, guessing instances would make instance synthesis unpredictable.
In some cases, however, the choice of one parameter should cause an automatic choice of another.
For example, the overloaded membership predicate type class Membership treats the type of elements of a data structure as an output, so that the type of element can be determined by the type of data structure at a use site, instead of requiring that there be sufficient type annotations to determine both types prior to starting instance synthesis.
An element of a ListNat can be concluded to be a Nat simply on the basis of its membership in the list.
Type class parameters can be declared as outputs by wrapping their types in the outParamgadget.
When a class parameter is an output, instance synthesis will not require that it be known; in fact, any existing value is ignored completely.
The first instance that matches the input parameters is selected, and that instance's assignment of the output parameter becomes its value.
If there was a pre-existing value, then it is compared with the assignment after synthesis is complete, and it is an error if they do not match.
Gadget for marking output parameters in type classes.
For example, the Membership class is defined as:
class Membership (α : outParam (Type u)) (γ : Type v)
This means that whenever a typeclass goal of the form Membership ?α ?γ comes
up, Lean will wait to solve it until ?γ is known, but then it will run
typeclass inference, and take the first solution it finds, for any value of ?α,
which thereby determines what ?α should be.
This expresses that in a term like a ∈ s, s might be a Set α or
List α or some other type with a membership operation, and in each case
the "member" type α is determined by looking at the container type.
Output Parameters and Stuck Search
This serialization framework provides a way to convert values to some underlying storage type:
example:=typeclass instance problem is stuck, it is often due to metavariables
Serialize (Nat × Nat) ?m.16ser(2,3)
Instance synthesis can't select the SerializeNatString instance, and thus the AppendString instance, because that would require instantiating the output type as String, so the search gets stuck:
typeclass instance problem is stuck, it is often due to metavariables
Serialize (Nat × Nat) ?m.16
One way to fix the problem is to supply an expected type:
example:String:=ser(2,3)
The other is to make the output type into an output parameter:
Now, instance synthesis is free to select the SerializeNatString instance, which solves the unknown implicit output parameter of ser:
example:=ser(2,3)Output Parameters with Pre-Existing Values
The class OneSmaller represents a way to transform non-maximal elements of a type into elements of a type that has one fewer elements.
There are two separate instances that can match an input type OptionBool, with different outputs:
Because instance synthesis selects the most recently defined instance, the following code is an error:
#checkfailed to synthesize
OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.OneSmaller.shrink(β:=Bool)(somefalse)sorry
failed to synthesize
OneSmaller (Option Bool) Bool
Additional diagnostic information may be available using the `set_option diagnostics true` command.
The OneSmaller(OptionBool)(OptionUnit) instance was selected during instance synthesis, without regard to the supplied value of β.
Semi-output parameters are like output parameters in that they are not required to be known prior to synthesis commencing; unlike output parameters, their values are taken into account when selecting instances.
Gadget for marking semi output parameters in type classes.
Semi-output parameters influence the order in which arguments to type class
instances are processed. Lean determines an order where all non-(semi-)output
parameters to the instance argument have to be figured out before attempting to
synthesize an argument (that is, they do not contain assignable metavariables
created during TC synthesis). This rules out instances such as [Mul β] : Add α (because β could be anything). Marking a parameter as semi-output is a
promise that instances of the type class will always fill in a value for that
parameter.
This means that all Coe instances should provide a concrete value for α
(i.e., not an assignable metavariable). An instance like Coe Nat Int or Coe α (Option α) is fine, but Coe α Nat is not since it does not provide a value
for α.
Semi-output parameters impose a requirement on instances: each instance of a class with semi-output parameters should determine the values of its semi-output parameters.
Semi-Output Parameters with Pre-Existing Values
The class OneSmaller represents a way to transform non-maximal elements of a type into elements of a type that one fewer elements.
It has two separate instances that can match an input type OptionBool, with different outputs:
Because instance synthesis takes semi-output parameters into account when selecting instances, the OneSmaller(OptionBool)(OptionUnit) instance is passed over due to the supplied value for β:
When instance synthesis would otherwise fail, having not selected an instance, the default instances specified using the default_instance attribute are attempted in order of priority.
When priorities are equal, more recently-defined default instances are chosen before earlier ones.
The first default instance that causes the search to succeed is chosen.
Default instances may induce further recursive instance search if the default instances themselves have instance-implicit parameters.
If the recursive search fails, the search process backtracks and the next default instance is tried.
3.6.3.7. “Morally Canonical” Instances
During instance synthesis, if a goal is fully known (that is, contains no metavariables) and search succeeds, no further instances will be attempted for that same goal.
In other words, when search succeeds for a goal in a way that can't be refuted by a subsequent increase in information, the goal will not be attempted again, even if there are other instances that could potentially have been used.
This optimization can prevent a failure in a later branch of an instance synthesis search from causing spurious backtracking that replaces a fast solution from an earlier branch with a slow exploration of a large state space.
The optimization relies on the assumption that instances are morally canonical.
Even if there is more than one potential implementation of a given type class's overloaded operations, or more than one way to synthesize an instance due to diamonds, any discovered instance should be considered as good as any other.
In other words, there's no need to consider all potential instances so long as one of them has been guaranteed to work.
The optimization may be disabled with the backwards-compatibility option backward.synthInstance.canonInstances, which may be removed in a future version of Lean.
Code that uses instance-implicit parameters should be prepared to consider all instances as equivalent.
In other words, it should be robust in the face of differences in synthesized instances.
When the code relies on instances in fact being equivalent, it should either explicitly manipulate instances (e.g. via local definitions, by saving them in structure fields, or having a structure inherit from the appropriate class) or it should make this dependency explicit in the type, so that different choices of instance lead to incompatible types.
Lean can automatically generate instances for many classes, a process known as deriving instances.
Instance deriving can be invoked either when defining a type or as a stand-alone command.
syntax
As part of a command that creates a new inductive type, a Lean.Parser.Command.declaration : commandderiving clause specifies a comma-separated list of class names for which instances should be generated:
The stand-alone Lean.Parser.Command.deriving : commandderiving command specifies a number of class names and subject names.
Each of the specified classes are derived for each of the specified subjects.
Instance deriving uses a table of deriving handlers that maps type class names to metaprograms that derive instances for them.
Deriving handlers may be added to the table using registerDerivingHandler, which should be called in an Lean.Parser.Command.initialize : commandinitialize block.
Each deriving handler should have the type ArrayName→CommandElabMBool.
When a user requests that an instance of a class be derived, its registered handlers are called one at a time.
They are provided with all of the names in the mutual block for which the instance is to be derived, and should either correctly derive an instance and return true or have no effect and return false.
When a handler returns true, no further handlers are called.
Lean includes deriving handlers for the following classes:
For datatypes that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive.
The instance for Bool is typical:
BEq α is a typeclass for supplying a boolean-valued equality relation on
α, notated as a == b. Unlike DecidableEq α (which uses a = b), this
is Bool valued instead of Prop valued, and it also does not have any
axioms like being reflexive or agreeing with =. It is mainly intended for
programming applications. See LawfulBEq for a version that requires that
== and = coincide.
Typically we prefer to put the "more variable" term on the left,
and the "more constant" term on the right.
LawfulBEq α is a typeclass which asserts that the BEq α implementation
(which supplies the a == b notation) coincides with logical equality a = b.
In other words, a == b implies a = b, and a == a is true.
Instance Constructor
LawfulBEq.mk.{u} {α : Type u} [BEqα]
(eq_of_beq : ∀ {a b : α},
(a == b) = true → a = b)
(rfl : ∀ {a : α}, (a == a) = true)
: LawfulBEqα
Methods
eq_of_beq
:
∀ {a b : α}, (a == b) = true → a = b
If a == b evaluates to true, then a and b are equal in the logic.
Decidable p is a data-carrying class that supplies a proof that p is
either true or false. It is equivalent to Bool (and in fact it has the
same code generation as Bool) together with a proof that the Bool is
true iff p is.
Decidable instances are used to infer "computation strategies" for
propositions, so that you can have the convenience of writing propositions
inside if statements and executing them (which actually executes the inferred
decidability instance instead of the proposition, which has no code).
If a proposition p is Decidable, then (by decide : p) will prove it by
evaluating the decidability instance to isTrue h and returning h.
Because Decidable carries data,
when writing @[simp] lemmas which include a Decidable instance on the LHS,
it is best to use {_ : Decidable p} rather than [Decidable p]
so that non-canonical instances can be found via unification rather than
typeclass search.
Constructors
isFalse {p : Prop} (h : ¬p) : _root_.Decidablep
Prove that p is decidable by supplying a proof of ¬p
isTrue {p : Prop} (h : p) : _root_.Decidablep
Prove that p is decidable by supplying a proof of p
Inhabited α is a typeclass that says that α has a designated element,
called (default : α). This is sometimes referred to as a "pointed type".
This class is used by functions that need to return a value of the type
when called "out of domain". For example, Array.get! arr i : α returns
a value of type α when arr : Array α, but if i is not in range of
the array, it reports a panic message, but this does not halt the program,
so it must still return a value of type α (and in fact this is required
for logical consistency), so in this case it returns default.
default is a function that produces a "default" element of any
Inhabited type. This element does not have any particular specified
properties, but it is often an all-zeroes value.
Nonempty α is a typeclass that says that α is not an empty type,
that is, there exists an element in the type. It differs from Inhabited α
in that Nonempty α is a Prop, which means that it does not actually carry
an element of α, only a proof that there exists such an element.
Given Nonempty α, you can construct an element of αnonconstructively
using Classical.choice.
a / b computes the result of dividing a by b.
The meaning of this notation is type-dependent.
For most types like Nat, Int, Rat, Real, a / 0 is defined to be 0.
For Nat, a / b rounds downwards.
For Int, a / b rounds downwards if b is positive or upwards if b is negative.
It is implemented as Int.ediv, the unique function satisfying
a % b + b * (a / b) = a and 0 ≤ a % b < natAbs b for b ≠ 0.
Other rounding conventions are available using the functions
Int.fdiv (floor rounding) and Int.div (truncation rounding).
For Float, a / 0 follows the IEEE 754 semantics for division,
usually resulting in inf or nan.
Pow.{u, v} (α : Type u) (β : Type v)
: Type (max u v)
The homogeneous version of HPow: a ^ b : α where a : α, b : β.
(The right argument is not the same as the left since we often want this even
in the homogeneous case.)
Types can choose to subscribe to particular defaulting behavior by providing
an instance to either NatPow or HomogeneousPow:
NatPow is for types whose exponents is preferentially a Nat.
HomogeneousPow is for types whose base and exponent are preferentially the same.
Instance Constructor
Pow.mk.{u, v} {α : Type u} {β : Type v}
(pow : α → β → α) : Powαβ
The homogeneous version of Pow where the exponent is a Nat.
The purpose of this class is that it provides a default Pow instance,
which can be used to specialize the exponent to Nat during elaboration.
For example, if x ^ 2 should preferentially elaborate with 2 : Nat then x's type should
provide an instance for this class.
The completely homogeneous version of Pow where the exponent has the same type as the base.
The purpose of this class is that it provides a default Pow instance,
which can be used to specialize the exponent to have the same type as the base's type during elaboration.
This is to say, a type should provide an instance for this class in case x ^ y should be elaborated
with both x and y having the same type.
For example, the Float type provides an instance of this class, which causes expressions
such as (2.2 ^ 2.2 : Float) to elaborate.
GetElem.{u, v, w} (coll : Type u) (idx : Type v)
(elem : outParam(Type w))
(valid : outParam (coll → idx → Prop))
: Type (max (max u v) w)
The classes GetElem and GetElem? implement lookup notation,
specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.
Both classes are indexed by types coll, idx, and elem which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation valid determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.
For example, an instance for arrays looks like
GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an
array xs and a natural number i, xs[i] will return an α when valid xs i
holds, which is true when i is less than the size of the array. Array
additionally supports indexing with USize instead of Nat.
In either case, because the bounds are checked at compile time,
no runtime check is required.
Given xs[i] with xs : coll and i : idx, Lean looks for an instance of
GetElem coll idx elem valid and uses this to infer the type of the return
value elem and side condition valid required to ensure xs[i] yields
a valid value of type elem. The tactic get_elem_tactic is
invoked to prove validity automatically. The xs[i]'p notation uses the
proof p to satisfy the validity condition.
If the proof p is long, it is often easier to place the
proof in the context using have, because get_elem_tactic tries
assumption.
The proof side-condition valid xs i is automatically dispatched by the
get_elem_tactic tactic; this tactic can be extended by adding more clauses to
get_elem_tactic_trivial using macro_rules.
xs[i]? and xs[i]! do not impose a proof obligation; the former returns
an Option elem, with none signalling that the value isn't present, and
the latter returns elem but panics if the value isn't there, returning
default : elem based on the Inhabited elem instance.
These are provided by the GetElem? class, for which there is a default instance
generated from a GetElem class as long as valid xs i is always decidable.
Important instances include:
arr[i] : α where arr : Array α and i : Nat or i : USize: does array
indexing with no runtime bounds check and a proof side goal i < arr.size.
l[i] : α where l : List α and i : Nat: index into a list, with proof
side goal i < l.length.
The syntax arr[i] gets the i'th element of the collection arr. If there
are proof side conditions to the application, they will be automatically
inferred by the get_elem_tactic tactic.
GetElem?.{u, v, w} (coll : Type u)
(idx : Type v) (elem : outParam(Type w))
(valid : outParam (coll → idx → Prop))
: Type (max (max u v) w)
The classes GetElem and GetElem? implement lookup notation,
specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.
Both classes are indexed by types coll, idx, and elem which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation valid determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.
For example, an instance for arrays looks like
GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an
array xs and a natural number i, xs[i] will return an α when valid xs i
holds, which is true when i is less than the size of the array. Array
additionally supports indexing with USize instead of Nat.
In either case, because the bounds are checked at compile time,
no runtime check is required.
Given xs[i] with xs : coll and i : idx, Lean looks for an instance of
GetElem coll idx elem valid and uses this to infer the type of the return
value elem and side condition valid required to ensure xs[i] yields
a valid value of type elem. The tactic get_elem_tactic is
invoked to prove validity automatically. The xs[i]'p notation uses the
proof p to satisfy the validity condition.
If the proof p is long, it is often easier to place the
proof in the context using have, because get_elem_tactic tries
assumption.
The proof side-condition valid xs i is automatically dispatched by the
get_elem_tactic tactic; this tactic can be extended by adding more clauses to
get_elem_tactic_trivial using macro_rules.
xs[i]? and xs[i]! do not impose a proof obligation; the former returns
an Option elem, with none signalling that the value isn't present, and
the latter returns elem but panics if the value isn't there, returning
default : elem based on the Inhabited elem instance.
These are provided by the GetElem? class, for which there is a default instance
generated from a GetElem class as long as valid xs i is always decidable.
Important instances include:
arr[i] : α where arr : Array α and i : Nat or i : USize: does array
indexing with no runtime bounds check and a proof side goal i < arr.size.
l[i] : α where l : List α and i : Nat: index into a list, with proof
side goal i < l.length.
The syntax arr[i]? gets the i'th element of the collection arr,
if it is present (and wraps it in some), and otherwise returns none.
getElem!
:
[inst : Inhabitedelem] → coll → idx → elem
The syntax arr[i]! gets the i'th element of the collection arr,
if it is present, and otherwise panics at runtime and returns the default term
from Inhabited elem.