Zulip Chat Archive

Stream: Is there code for X?

Topic: auto-coercions


view this post on Zulip Kyle Miller (Sep 18 2020 at 19:40):

What's the mechanism in Lean that inserts automatic coercions for functions? Here's an example:

example {α β : Type} (f : α  β) : function.injective f := ...

Lean inserts a coercion arrow, so it's actually function.injective ⇑f.

(Is this something can be enabled for other types? I'd imagine you give a type and a coercion function, and then when you pass an argument to a function that doesn't have the expected type, the expected type's coercion function is inserted.)

view this post on Zulip Floris van Doorn (Sep 18 2020 at 19:43):

There is a minimal amount of documentation of this feature in this file: https://github.com/leanprover-community/lean/blob/master/library/init/coe.lean

view this post on Zulip Kyle Miller (Sep 18 2020 at 19:43):

An example application: if a structure B extends another structure A, you cannot pass something of type B to a function expecting something of type A, but it would be convenient if Lean automatically inserted the B.to_A function.

view this post on Zulip Floris van Doorn (Sep 18 2020 at 19:44):

Also https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes

view this post on Zulip Floris van Doorn (Sep 18 2020 at 19:45):

I think in Lean 2 a coercion from an extended structure to the original structure was automatically generated.
In Lean 3 / mathlib almost all extending of structures actually happens on classes, so that feature is not very applicable.

view this post on Zulip Floris van Doorn (Sep 18 2020 at 19:46):

The basic usage is that if you define

instance : has_coe B A := ...

then a coercion from B to A is automatically inserted.

view this post on Zulip Floris van Doorn (Sep 18 2020 at 19:47):

Also look at the variants docs#has_coe_to_fun and docs#has_coe_to_sort

view this post on Zulip Kyle Miller (Sep 18 2020 at 19:47):

What's nice about has_coe_to_fun is that the coercion is able to direct the type it gets coerced to, but has_coe cannot, so it sometimes needs some help with explicit type annotations.

I've noticed that classes are used to do this sort of polymorphism, but not everything can be a class because there aren't always good parameters to attach them to.

view this post on Zulip Kyle Miller (Sep 18 2020 at 19:48):

I was imagining, in certain cases, being able to define your own has_coe_to_fun-like thing where the thing being coerced can specify some of the type variables in the coercion.

view this post on Zulip Kyle Miller (Sep 18 2020 at 19:50):

Should I take it that somewhere deep in the elaborator, Lean 3 knows about has_coe_to_fun and will automatically insert coercions?

view this post on Zulip Floris van Doorn (Sep 18 2020 at 20:02):

Yeah, has_coe, has_coe_to_fun and has_coe_to_sort are hard-coded somewhere in the elaborator in C++.

view this post on Zulip Kyle Miller (Sep 18 2020 at 20:13):

Assuming for a moment it makes sense to have structures with no parameters, is there any way to get this coercion to work? The class resolution trace says "failed is_def_eq", which I think is because it's not able to solve for the universe variables -- there's no way to tell has_coe that has_coe (B a) A.{v} does not exist for v not equal to u.

universes u

structure A :=
(X : Type u)

structure B (a : A) :=
(X' : set a.X)

def B.to_A {a : A} (b : B a) : A :=
{ X := subtype b.X' }

instance B_to_A' (a : A) : has_coe (B a) A :=
{ coe := B.to_A }

-- "A.X b" is not ok, since cannot coerce b to be of type A
example (a : A) (b : B a) :  (x : A.X b), x = x := sorry

-- OK
example (a : A) (b : B a) :  (x : A.X b.to_A), x = x := sorry

-- OK
example (a : A.{u}) (b : B a) :  (x : A.X.{u} b), x = x := sorry

view this post on Zulip Kyle Miller (Sep 18 2020 at 20:19):

This would work:

universes u v

structure A :=
(X : Type u)

structure B (a : A) :=
(X' : set a.X)

def B.to_A {a : A} (b : B a) : A :=
{ X := subtype b.X' }

class has_coe_to_A (β : Type u) :=
(coe : β  A.{v})

notation ``:max x:max := has_coe_to_A.coe x

instance (a : A) : has_coe_to_A (B a) :=
{ coe := B.to_A }

example (a : A) (b : B a) :  (x : A.X b), x = x := sorry

It'd be nice if the could be automatically inserted.

view this post on Zulip Reid Barton (Sep 18 2020 at 20:21):

I haven't looked at your example closely, but I thought that Lean no longer hesitates to use an instance even if it would mean assigning a universe level metavariable.

view this post on Zulip Kyle Miller (Sep 18 2020 at 20:27):

With the first setup, here's a pair where the only difference is whether both universes are explicitly given:

example (a : A.{u}) (b : B a) :  (x : A.X b), x = x := sorry  -- not OK
example (a : A.{u}) (b : B a) :  (x : A.X.{u} b), x = x := sorry -- OK

view this post on Zulip Reid Barton (Sep 18 2020 at 20:27):

Did I imagine that? It does quite look like that is what is going wrong

view this post on Zulip Reid Barton (Sep 18 2020 at 20:32):

I guess I was thinking of https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.233221.20remove.20universe.20annotations.20in.20category_theory/near/202266781 but it seems that nobody really knows what happened there.

view this post on Zulip Kyle Miller (Sep 18 2020 at 20:41):

That's amusing no one really knows what happened -- I guess I should take closer look at the category theory library to see what it's doing that might help class resolution out. Do you think that this B_to_A coercion should work in principle?

view this post on Zulip Kyle Miller (Sep 21 2020 at 19:12):

Thanks @Floris van Doorn and @Reid Barton for your comments and for helping me understand auto-coercions better. I didn't realize that has_coe.coe was automatically inserted, probably because in my application (the simple graphs API) it didn't obviously work so I didn't think to inspect the class resolution trace.

Would it be possible or reasonable to make it so that class resolution will use an instance to solve for universe metavariables in the special case that they are unconstrained by the type variables? The underlying assumption is that no one would ever define any other instances, so, using the language of logic programming, it's seems safe to take a closed-world assumption here.

The #mwe from above is supposed to represent a structure that is not naturally a class (i.e., mathematical objects that are not referred to by synecdoche) that has a notion of sub-object -- and from the perspective of objects that are referred to by synecdoche (i.e., pretty much algebraic object in mathlib), it's a bundled structure. Everything I've been going on about with the synecdoche problem this summer seems like it would be resolved if this has_coe instance would work.

In the meantime, I've reorganized the simple_graphs2 branch, which has been a test-bed for experimenting with different approaches, to use a custom coercion class and coercion arrow that is specifically for coercion to simple graphs. This enforces that the universe is a function of the type being coerced.

The arrow is defined here. It's not so bad putting the arrow where it's needed, but it would just be a little more convenient not having to place the arrows at all.

(The way this differs from what I was doing before is that, before you'd essentially have to prove all your generic theorems with respect to types that have a has_coe_to_simple_graph instance. It was ok, but it always felt awkward, and it made some constructions more difficult than they needed to be, I think. Recently I gained some confidence that structures with unconstrained universe variables would be OK, and it does seem to work out fine for simple graphs.)

view this post on Zulip Kyle Miller (Sep 21 2020 at 19:13):

I didn't want to break convention with coercion arrows, but something I noticed is that if it instead were a postfix operation

postfix `  `:max_plus

then you can write stuff like G↟.adj rather than (↟G).adj

view this post on Zulip Kyle Miller (Sep 21 2020 at 19:15):

(It's reminiscent of how in Pascal, they used a postfix pointer dereferencing operator. Using C-like notation, you can do x*.foo rather than needing a separate x->foo.)

view this post on Zulip Kyle Miller (Sep 21 2020 at 19:23):

Another reason not defining it this way, beyond convention, is that using this postfix arrow along with generalized field access notation means it can't be seamlessly be replaced by has_coe, due to the fact that the field access notation needs to be able to determine the name of the type to resolve. Still, it seems like nice notational hack to consider.

view this post on Zulip Floris van Doorn (Sep 21 2020 at 20:54):

I think generally we want to coerce objects only to other objects of the same universe (or at least, a universe determined by the object in question). I don't know how hard it is to change the type-class mechanism to incorporate your suggestion
Why doesn't has_coe (simple_graph_on V) simple_graph, or any of your other examples, work? It looks like the universe of the target is the same (or at least determined) by the coerced object.
Also, I would encourage you to not add too many coercions. The coercions from simple_graph_on and of_edge_set' should probably just be named operations. The former is very similar to docs#category_theory.bundled whose constructor is also not a coercion.
I feel strongly that we should not have a dedicated global notation to coerce specifically to simple_graph.

view this post on Zulip Kyle Miller (Sep 21 2020 at 21:46):

The issue with has_coe (simple_graph_on V) simple_graph is that Lean can figure out the universe for simple_graph_on V, so then it would know how to coerce to simple_graph.{u} for V : Type u, but then class inference can't make the leap that this instance should be used, because all it knows is that it needs a simple_graph.{v} for some v. I assume it's because someone might later introduce an instance like has_coe (simple_graph_on V) simple_graph.{u+1}, even though we know this is highly unlikely.

I agree I don't need of_edge_set' to have a coercion -- it's only there to show that two ways of defining subgraphs are equivalent and it should only be a local instance -- but it's useful having simple_graph_on being coerceable. There are many cases where you'd like ready access to the vertex type for rewriting, so it's worth making things like path_graph be a simple_graph_on rather than a simple_graph when possible -- and ideally you wouldn't need to pervasively clutter code with casts to the simple_graph type. One place it's useful is in working with walks in a graph as homomorphisms ↟(path_graph length) →g G, where the vertex type is fin (length + 1). In any case, there are only really two types right now where it's convenient to have a coercion to simple_graph: simple_graph_on and subgraph. There probably wouldn't ever be many more than this.

I also agree that there shouldn't be a dedicated global notation for coercing to simple graphs. I'm hoping has_coe will work and then it can be removed entirely. But if not, then I can revert to the method I was previously using without too many changes, or I can just give the tree arrow as local notation. (An audacious proposal is for this to be a special coercion notation that is overloaded for specific coercion destinations. Like how :: is overloaded.)


Last updated: May 17 2021 at 16:26 UTC