Lean 4 set_like

Stream: lean4

[Kevin Buzzard]

I'll be the first to admit I don't understand all this coe_t stuff. Here in Lean 3's mathlib there's a has_coe_t instance for a very simple structure:

set_option old_structure_cmd true

/-- A class to indicate that there is a canonical injection between `A` and `set B`. -/
@[protect_proj]
class set_like (A : Type*) (B : out_param $ Type*) :=
(coe : A → set B)
(coe_injective' : function.injective coe)

namespace set_like

variables {A : Type*} {B : Type*} [i : set_like A B]

include i

instance : has_coe_t A (set B) := ⟨set_like.coe⟩

How should the has_coe_t be translated into Lean 4?

[Kevin Buzzard]

I may as well ask about the next part too:

@[priority 100]
instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩

-- `dangerous_instance` does not know that `B` is used only as an `out_param`
@[nolint dangerous_instance, priority 100]
instance : has_coe_to_sort A := ⟨_, λ p, {x : B // x ∈ p}⟩

Can Lean 4 do priorities and should these be low in Lean 4? I've seen priority := low in lean 4 but only for macros.

[Kevin Buzzard]

This compiles (if you've defined Set, e.g. like in mathlib4)

variable {A : Type u} {B : Type v} [i : set_like A B]

instance [i : set_like A B] : CoeT A a (Set B) := ⟨set_like.coe a⟩

but I don't know if I'm supposed to be using CoeT in Lean 4 because I understand what's going on properly yet.

[Daniel Selsam]

Kevin Buzzard said:

How should the has_coe_t be translated into Lean 4?

The direct translation seems to work:

def Set (α : Type u) := α → Prop

def Injective (f : α → β) : Prop :=
  ∀ x y, f x = f y → x = y

class SetLike (A : Type u) (B : outParam (Type v)) where
  (coe : A → Set B)
  (coeInjective : Injective coe)

instance [SetLike α β] : Coe α (Set β) := ⟨SetLike.coe⟩

Are you asking about the _t part in particular? Or is it not finding the coercion later on when you expect it to?

[Daniel Selsam]

Kevin Buzzard said:

Can Lean 4 do priorities and should these be low in Lean 4? I've seen priority := low in lean 4 but only for macros.

Yes, this works:

class Foo where
  x : Bool

instance (priority := low)  : Foo := ⟨true⟩
example : Foo.x = true := rfl

instance (priority := high) : Foo := ⟨false⟩
example : Foo.x = false := rfl

instance (priority := low) : Foo := ⟨true⟩
example : Foo.x = false := rfl

[Kevin Buzzard]

Daniel Selsam said:

Are you asking about the _t part in particular? Or is it not finding the coercion later on when you expect it to?

Exactly -- I don't know what coe_t means. I see that your Lean 4 translation of the Lean 3 code uses Coe. Because I don't understand why coe_t was used in Lean 3 (@Eric Wieser ?) and I also don't understand the differences between the Lean 3 and Lean 4 type class algorithm, I am unclear about how to port this file correctly.

[Mac]

Kevin Buzzard said:

Exactly -- I don't know what coe_t means. I see that your Lean 4 translation of the Lean 3 code uses Coe. Because I don't understand why coe_t was used in Lean 3 (Eric Wieser ?) and I also don't understand the differences between the Lean 3 and Lean 4 type class algorithm, I am unclear about how to port this file correctly.

Lean 4 also has its coe_t, named CoeT. To quote the definition of CoeT in the source, it:
"Combines CoeHead, CoeTC, CoeTail, CoeDep" where CoeHead is for expensive initial coercions, CoeTC is the transitive closure of Coe, CoeTail is for expensive final coercions, CoeDep for dependently-typed coercions. In essence, CoeT is the sum of all the basic term coercions. The Coe library also includes CoeHTCT for when you don't need CoeDep in the mix.

[Kevin Buzzard]

The problem is that I am a mathematician and have no concept of what is expensive, for me maths runs at infinite speed and all these coercions are obvious.

[Mac]

Then just define Coe instances use CoeT in class constraints and let those with more CS experience who notice slowdowns redefine them as needed. ;)

[Gabriel Ebner]

Kevin Buzzard said:

How should the has_coe_t be translated into Lean 4?

A lot of people here have already commented on what the Coe* classes do in Lean 4, but nobody has mentioned so far why we're using has_coe_t in Lean 3 in the first place. The reason is simple: termination. We want all type-class query to terminate, quickly, and no matter whether they fail or succeed.

Therefore the general rule is that coercion instances where (simplifying a bit) one side is a variable must be has_coe_t instead of has_coe. For example has_coe α (option α) would be super bad, since you can chain it transitively to has_coe α (option (option α)), etc. Type class synthesis has changed considerably in Lean 4, but I believe this source of nontermination is still present.

For the set_like coercion, nontermination of transitive chaining is not an issue in practice. This is because all set_like instances are all of the form set_like (subsemiring R) R. Therefore it is ok to use Coe for set_like. (The mathlib linter rightfully complains, since it doesn't know about this special invariant of the declared set_like instances).

instance [SetLike A B] : Coe A (Set B) where
  coe := set_like.coe

(or even better, make SetLike extend Coe)

[Gabriel Ebner]

Kevin Buzzard said:

Can Lean 4 do priorities and should these be low in Lean 4? I've seen priority := low in lean 4 but only for macros.

The relevant question here is not "can Lean 4 do priorities" but "why are we using them in Lean 3". Almost all occurrences of instance priorities are to work around performance issues with type class synthesis, as described in this library note: https://leanprover-community.github.io/mathlib_docs/notes.html#lower%20instance%20priority

Therefore I would suggest to leave out the instance priorities in Lean 4 code for now, until we have a better idea about the performance cliffs of the new type class synthesis algorithm.

Side note: instance priorities are extremely finicky, and should be avoided except as a last resort when you absolutely know what you're doing.

[Mac]

Gabriel Ebner said:

Kevin Buzzard said:

How should the has_coe_t be translated into Lean 4?

A lot of people here have already commented on what the Coe* classes do in Lean 4, but nobody has mentioned so far why we're using has_coe_t in Lean 3 in the first place. The reason is simple: termination. We want all type-class query to terminate, quickly, and no matter whether they fail or succeed.

For example has_coe α (option α) would be super bad, since you can chain it transitively to has_coe α (option (option α)), etc. Type class synthesis has changed considerably in Lean 4, but I believe this source of nontermination is still present.

In that case, in Lean 4, you would want to always use Coe rather than CoeT, as CoeT is the full super transitive closure. Right?

[Gabriel Ebner]

Coe is of course still bad because it is chained transitively. You can now choose between CoeHead, CoeTC, CoeTail, CoeHTCT, and CoeT for the option coercion, since none of these are chained. (The core Lean 4 library chooses CoeTail.)

[Mac]

On a separate question:

Gabriel Ebner said:

Side note: instance priorities are extremely finicky, and should be avoided except as a last resort when you absolutely know what you're doing.

They are? Sebastian had me use them for properly ordering derivative MonadReader/MonadState instances (see this Zulip thread) and his statements there made it sound like they were the preferred way to do that.

[Mac]

Gabriel Ebner said:

Coe is of course still bad because it is chained transitively. You can now choose between CoeHead, CoeTC, CoeTail, CoeHTCT, and CoeT for the option coercion, since none of these are chained. (The core Lean 4 library chooses CoeTail.)

I'm confused. So a Coe constraint is bad because it is a link in the chain? I would think the transitive classes themselves (i.e., CoeHTCT/ CoeT) would be the problem for nontermination, not the Coe links in the chian.

[Sebastian Ullrich]

The monad classes are a rare case where we explicitly want overlapping instances to solve mtl's "n * m instances* problem. We carefully select paths through the diamonds created by the overlapping via priorities (or declaration order).

[Gabriel Ebner]

Mac said:

I'm confused. So a Coe constraint is bad because it is a link in the chain? I would think the transitive classes themselves (i.e., CoeHTCT/ CoeT) would be the problem for nontermination, not the Coe links in the chian.

I'm not talking about constraints. Declaring a Coe instance can be bad, because the coercion mechanism looks for a CoeT instance---and this can apply the Coe instance an unbounded number of times.

[Mac]

Ah, I misunderstood. I thought you were talking about constraints not declarations. In that case, yeah, CoeHead/CoeTail are the goto classes.

[Gabriel Ebner]

My comment about instance priorities was directed at the "I want a different addition on Nat, so I'm going to declare instance (priority := high) : AddMonoid Nat" idea I see sometimes.

[Mac]

That would still work, right? As that goes to overlapping instance idea that Sebastian mentioned. It is, however, an admittedly less than ideal usage,, though.

[Gabriel Ebner]

It probably doesn't work: when Lean looks for a Add Nat instance it most likely tries instAddNat first instead of AddMonoid.toAdd (because you've only changed the priority of the AddMonoid instance, but not of any Add instances).

[Mac]

Ah, makes sense! That is a really good example of what kind of brittleness instance priorities have.