The meaning of instances

Stream: new members

[Jeremy Tan]

Just what is an instance in Lean 4 and how does it differ from definitions/theorems?

[Henrik Böving]

It is an instance of a type class. If you dont know what type classes are, similar systems are known under names like trait (in .e.g Rust) or also the weaker interface concept from e.g. Java.

And technically speaking since type classes are (except for class inductive variations but those are very rare) structures an instance is actually only definition with a value of some structure with some tag that makes it special to the compiler. But that is more of a detail

[Kevin Buzzard]

There's a good explanation in #tpil

[Somo S.]

@Henrik Böving said:

except for class inductive variations but those are very rare

Following up on class inductive (archived topic), what then is the syntax for creating an "instance" of a class inductive?
I haven't seen this explained anywhere in #tpil

[Anne Baanen]

The syntax should be exactly the same as creating a def of the same type, except the name is optional for an instance.

[Somo S.]

from #fpil

Behind the scenes, type classes are structure types and instances are values of these types. The only differences are that Lean stores additional information about type classes, such as which parameters are output parameters, and that instances are registered for searching.

I am not sure I understand @Anne Baanen. If you use a def to declare your class inductive instance value, will Lean properly register that value for class searching (and store output parameters etc) as is described above (for regular structure based class types)

[Anne Baanen]

In the foundational logic there is no difference at all between class inductive and inductive, or class and structure, or instance and def, all of these pairs are translated to the same core concepts. In fact, a structure is just an inductive with only one constructor. This is what TPiL means by "behind the scenes".

The difference comes in the translation from your code to these foundations, where a part of Lean called the elaborator fills in all the implicit arguments, the ones between {curly braces} (implicit parameters) and [square braces] (instance parameters). When trying to fill in an instance parameter, Lean essentially does a depth-first search until it finds something with the right type. And the set of declarations it searches through is exactly those that have been declared an instance instead of a plain def.

Even more precisely, an instance is just a def together with an attribute @[instance]. The instance keyword assigns this attribute automatically, or you can do this manually by writing attribute [instance] your_def. Similarly, a class is just any declaration with an attribute @[class]. Lean 3 doesn't actually check that the attribute is on an inductive type.

So what this means in practice for a class inductive like docs#decidable is that declaring an instance works exactly the same: you construct a term of the type, like docs#and.decidable, and as long as it gets the @[instance] attribute (either through the instance keyword or attribute [instance] and.decidable), it will function like any other class instance.

Does that help or is there still something unclear?

[Somo S.]

actually this all makes sense now. the links you provided showed me example code. Thanks @Anne Baanen