Instances in constructors

Stream: general

[Robert Maxton]

Suppose I have

class Foo (α : Type u) where
  β : Type u
  inj (α) : β → α

structure Bar where
  α : Type u
  [foo : Foo α]
  inj' : Foo.β α → α

attribute [instance] Bar.foo

This much works fine: Lean recognizes that the instance foo exists and lets you write Foo.β α in the type of inj'.

But, when you try to make a Bar:

def bar : Bar where
  α := PUnit
  foo := ⟨PEmpty, PEmpty.elim⟩
  inj' := Foo.inj PUnit -- failed to synthesize Foo PUnit

Within the definition, the instance isn't visible.

I imagine that this is an example of the more general difficulty with constructors, that there's no good way to directly make reuse field values in other fields without doing let := ...; { ... }. Nevertheless, it complicates the construction of complex structures, and I'd like to see what workarounds exist.

[Kyle Miller]

It's a difficulty with function applications in general: just because you have explicitly provided an instance for an instance argument doesn't mean it should be made available as an instance to the later arguments.

One could imagine there should be an exception here, but it seems like it makes more sense for where notation than {...} notation, and we want these to be consistent (where is pretty much a macro for {...}).

A design idea that once crossed my mind though would be to have some syntax that means "lift this field as a let". For example, you might have

def bar : Bar where
  α := PUnit
  let foo := ⟨PEmpty, PEmpty.elim⟩
  inj' := Foo.inj PUnit

mean

def bar : Bar :=
  let foo := ⟨PEmpty, PEmpty.elim⟩
  { α := PUnit
    foo
    inj' := Foo.inj PUnit }

[Kyle Miller]

However, there'd need to be some smarts here beyond a simple macro, since foo needs a type for it to be registered as a local instance.

def bar : Bar :=
  let foo : Foo PUnit := ⟨PEmpty, PEmpty.elim⟩
  { α := PUnit
    foo
    inj' := Foo.inj PUnit }

[Robert Maxton]

One thing I came up with was changing the type of inj' to [Foo α] → Foo.β α → α, which basically does the trick of "letting you define a field value as if another field value was in scope" so long as you have the attribute [instance] on Bar.foo.

[Kyle Miller]

The let type isn't the only complication with this. Then there's the question of "what should have this let be in scope?" The natural thing is all the remaining fields in the structure's field order, but that disagrees with what's visible in the source code (you're allowed to provide fields in any order you want, but they always elaborate in the structure's field order).

[Kyle Miller]

Robert Maxton said:

One thing I came up with was [...]

Interesting trick, though doesn't that change the meaning so that inj' is no longer about just foo, but any Foo instance?

[Kyle Miller]

Right now, this is how we've expected people to introduce local instances:

def bar : Bar :=
  let : Foo PUnit := ⟨PEmpty, PEmpty.elim⟩
  { α := PUnit
    inj' := Foo.inj PUnit }

I think the syntaxes are aligned well enough that you can always transform where $flds to := { $flds } and it will work. Last year { ... } didn't support everything where did.

[Robert Maxton]

Kyle Miller said:

A design idea that once crossed my mind though would be to have some syntax that means "lift this field as a let".

For the specific case of instances, it might be intuitive to just enable [...] in the body of the where:

def bar : Bar where
  α := PUnit
  [foo := ⟨PEmpty, PEmpty.elim⟩]
  inj' := Foo.inj PUnit

And then, since it's imitating let foo := ...; { ... } anyway, basically do the same sort of thing as generalize, hoisting both the given definition and everything it depends on to above the structure constructor and replacing values with references?

[Robert Maxton]

Kyle Miller said:

Robert Maxton said:

One thing I came up with was [...]

Interesting trick, though doesn't that change the meaning so that inj' is no longer about just foo, but any Foo instance?

Yes, this is definitely leaning on the "we kind of want instances to be subsingletons" expectation, and works best with Prop-valued classes.

(... which this example isn't lol, but my original inspiring use case was)

[Kyle Miller]

Square brackets don't seem to be any different from let with the ordering problem. Quick example:

def bar : Bar where
  α := PUnit
  inj' := Foo.inj PUnit
  [foo := ⟨PEmpty, PEmpty.elim⟩]

Would you be surprised that foo is an instance for inj'?

Another example:

structure Baz where
  α : Type u
  eq : (x y : α) → Bool
  [inst : DecidableEq α]

def MyNat := Nat

def Nat.baz : Baz where
  α := MyNat
  [inst := instDecidableEqNat]
  eq := fun x y => decide (x = y)

Would you be surprised that eq might not be able to use the DecidableEq instance? (If it did a full dependency analysis rather than elaborate fields in structure order, then this particular example would work, but there must be examples where the instance would appear first and you want it in a field that's written later, but some field dependency that might not be a dependency given the concrete values of the fields may prevent that. Seems counterintuitive, and I think it would make it more unpredictable.)

[Robert Maxton]

Kyle Miller said:

Would you be surprised that foo is an instance for inj'?

Depends on how well it was documented :p . My suggestion is "unconditionally hoist 'highlighted' fields" (whether by [..] or let or otherwise) "and all dependents all the way to the top, so that they are visible in all later fields"; which could be surprising, but at least it would be consistent, and if the notation came with a hover-doc the surprise would be limited. (Also, the reason I'm focusing on [..] is that instances I feel have a special place here; while indeed you might be very surprised if a variable you define was visible 'before' its definition, I think that you'd be much less surprised if an instance, something intuitively kind of 'ambient'/'external' anyway, had the same behavior.)

I also vaguely suspect that this is a sufficiently common use case that having an extra opt-in feature would be valuable even if it didn't work for all possible use cases, but that's something that would need to be justified with evidence.