Zulip Chat Archive

Stream: lean4

Topic: Default instances


view this post on Zulip François G. Dorais (Mar 12 2021 at 21:07):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:18):

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

view this post on Zulip Leonardo de Moura (Mar 12 2021 at 21:23):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:31):

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.

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:34):

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...

view this post on Zulip Mario Carneiro (Mar 12 2021 at 21:35):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:36):

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

view this post on Zulip Jason Gross (Mar 12 2021 at 21:41):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 21:49):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:52):

@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?

view this post on Zulip Mario Carneiro (Mar 12 2021 at 21:53):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 21:55):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 21:56):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:57):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 21:57):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 22:09):

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

view this post on Zulip Jason Gross (Mar 12 2021 at 22:40):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 22:43):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 22:44):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 22:45):

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 (+)

view this post on Zulip Mario Carneiro (Mar 12 2021 at 22:46):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 22:46):

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

view this post on Zulip François G. Dorais (Mar 12 2021 at 22:53):

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.

view this post on Zulip François G. Dorais (Mar 12 2021 at 23:09):

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

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 02:59):

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.


Last updated: May 07 2021 at 13:21 UTC