Default instances

Stream: lean4

[François G. Dorais]

What is the difference between having a default instance and having a very low priority instance?

[François G. Dorais]

In other words, what is a context where I should prefer a default instance over a very low priority instance?

[Leonardo de Moura]

https://leanprover.github.io/lean4/doc/typeclass.html#default-instances

[François G. Dorais]

I had just read that before asking, so my question wasn't precise enough... Sorry! What is a context (other than heterogeneous operators) where I would somehow expect class synthesis to be pending and default instances to kick in? (Assuming I understood that section correctly.) The heterogeneous operator makes sense since the argument types can all be metavariables that can't be inferred unambiguously, I'm wondering how this feature could be useful in different contexts.

[François G. Dorais]

PS: I'm trying to figure out what's unclear to me but I think I will only figure out what is unclear once it becomes clear... Maybe I need to rethink this question entirely...

[Mario Carneiro]

If it helps, another example of default instances from lean 3 is nat literal defaulting: 0 : ?M has lots of possible instances but ?m := nat is a default instance

[François G. Dorais]

But isn't that just a low priority instance? (Lean 3 doesn't have default instances, does it?)

[Jason Gross]

In Lean 4, typeclass resolution does not trigger on goals when non-outParam class arguments have metavariables. It seems like default instances do trigger here

[Mario Carneiro]

François G. Dorais said:

(Lean 3 doesn't have default instances, does it?)

Lean 3 has exactly one "default instance", which is nat defaulting. Lean 4 generalized the mechanism to default instances

[François G. Dorais]

@Mario Carneiro I'm sure that is incredibly useful, especially with normalization and such. What would go wrong in Lean 3 with non-meta code if that were just a low priority instance?

[Mario Carneiro]

I don't see how it being an instance of any priority would help. There is nothing in the typeclass system that suggests that nat should get involved

[Mario Carneiro]

I think Jason Gross has the right idea. Since the type of the variable is not an out_param (to, say, has_zero A), lean will not unify it even though it knows has_zero nat, so if you write #eval 0 you would just get a type error saying it can't infer the type of 0

[Mario Carneiro]

I'm pretty sure the reason nat defaulting exists in lean 3 is so that #eval 2 + 2 will "just work"

[François G. Dorais]

Ah! I think I just got it thanks to @Mario Carneiro and @Jason Gross. I thought Lean 4 would just sew more roots in the forest to see if any one germinates but I guess that's not part of the algorithm from https://arxiv.org/pdf/2001.04301.pdf

[François G. Dorais]

I need to spend more time on that paper...

[François G. Dorais]

All the examples so far involve notation. Is there another way where default instances would trigger?

[Jason Gross]

If you want to be able to avoid ever needing to write coeSort explicitly, I guess you could add a default instance showing CoeSort -> Coe

[Mario Carneiro]

I can imagine using default instances for fully unbundled typeclasses like IsMonoid Nat 0 (+), where 0 and (+) are supplied via a default instance so that you can also use IsMonoid Nat 0 max

[François G. Dorais]

But how would that work, @Mario Carneiro , since + and max have the same signature?

[Mario Carneiro]

They would be inputs, i.e. if you need IsMonoit Nat 0 max or IsMonoid Nat 0 (+) you get it but if you search for IsMonoid Nat ? ? you get IsMonoid Nat 0 (+)

[Mario Carneiro]

that might happen if you rewrite with generic_assoc on a goal of max x (max y z) = 0

[Mario Carneiro]

that said, I'm not seriously proposing such a structure for mathlib or anything, I think there are a number of technical issues with a design like this

[François G. Dorais]

By the way, @Mario Carneiro, I did a big experiment a while ago that you might want to check out: https://github.com/fgdorais/lean-universal A lot of the hacks are really bad but it kinda works pretty well in Lean 3. Porting to Lean 4 is really challenging but I'm working on it to see whether this kind of approach is viable.

[François G. Dorais]

I sent @Mario Carneiro an invite in case you want to see how the Lean 4 port is progressing.

[Leonardo de Moura]

Mario Carneiro said:

François G. Dorais said:

(Lean 3 doesn't have default instances, does it?)

Lean 3 has exactly one "default instance", which is nat defaulting. Lean 4 generalized the mechanism to default instances

Correct.
Default instances are also crucial for implementing heterogeneous operators. https://leanprover.github.io/lean4/doc/typeclass.html#default-instances
Note that, we have a default instance for the scientific notation that defaults to Float, but users can redefine it to Real if they want.
It also allows gives flexibility to users. For example, the default instance for scientific notation is Float

#check 10.23 -- Float
#check 10.23e12 -- Float

but users can redefine it to be Real.

Default instances are not part of the type class resolution procedure, but a mechanism implemented in the elaborator.
The elaborator has a "to-do" list, and it tries to apply default instances when it cannot make progress. The to-do list contains pending typeclass resolution problems, and the elaborator tries to solve them using default instances.

I recommend you use default instances sporadically because they often create counterintuitive behavior. Haskell implements a similar mechanism, and if I remember correctly only the Haskell prelude defines default instances.