structure with unassigned variable as default variable

Stream: lean4

[David Renshaw]

structure Foo :=
  (x : Nat := 10) -- field of type `Nat` with default value `10`
  (y : Nat := foobar) -- field of type `Nat` with default value `foobar` ... ?

#print Foo.mk
-- constructor Foo.mk : (x : Nat) → ({x : Type} → {foobar : Nat} → Nat) → Foo

[David Renshaw]

^ I'm trying to understand what's happening here.

[David Renshaw]

I expect the structure declaration to cause an error, because foobar is an undeclared variable.

[David Renshaw]

Instead, it succeeds and apparently creates a field of type ({x : Type} → {foobar : Nat} → Nat)

[Yakov Pechersky]

I think it is doing implicit argument placement

[Henrik Böving]

First things first style wise we'd do:

structure Foo where
  x : Nat := 10
  y : Nat := foobar

in Lean 4, the foobar is being treated as an implicit argument as Yakov suggested, and in order to accommodate that implicit variable Lean ends up creating quite an interesting type that you can see here. The eagerness of auto implicit has been subject to discussion before and there are some ideas around on how we could turn it down.

[David Renshaw]

I was also wondering about the difference between where and :=

[Sebastian Ullrich]

No semantic difference

[Henrik Böving]

Maybe we should get rid off := for structures and classes at some point then to enforce the generally accepted style guide easier?

[David Renshaw]

I can maybe understand that foobar is added as an autoimplicit, but what about the added {x : Type} implicit parameter?

[Henrik Böving]

I'm not quite sure where it is pulling that one from either but its most likely a cause of the autoImplicit feature trying to do its job.

[Sebastian Ullrich]

Huh, that's strange

[Sebastian Ullrich]

In any case, I can't think of any reason to allow auto implicits in default values

[Mac]

Henrik Böving said:

Maybe we should get rid off := for structures and classes at some point then to enforce the generally accepted style guide easier?

One use case of the := is in macros where constructing such a structure can be easier, but I am doubtful that would be a good enough reason to keep the alternative syntax around.

[Mac]

David Renshaw said:

about the added {x : Type} implicit parameter?

I imagine that is a by product of the interaction between auto implicits and the way default values for structures work. That is, the default value of a each field has invisible arguments corresponding to the values of the previous fields (e.g., x) and I think the auto implicit mechanic has accidently lifted this invisible argument into a type while lifting foobar (likely because the elimination procedure for x failed because foobar is a metavariable so it can not be sure if x was used in foobar until later when auto-implicits come in).

[Henrik Böving]

It is not the x from the first parameter, if you name the first one different:

structure Foo where
  lalala : Nat := 10
  y : Nat := foobar

#check Foo.mk

you get

Foo.mk : Nat → ({x : Type} → {foobar : Nat} → Nat) → Foo

and it also happens if there is only a single field.

[Mac]

Ah, probably should have checked before commenting.

[Mac]

Interesting, the type is always one universe higher than that of the param:

structure Baz :=
  (y : Type 2 := foobar)

#print Baz.mk
-- constructor Baz.mk : ({x : Type 3} → {foobar : Type 2} → Type 2) → Baz

[Mac]

Maybe it is the polymorphic type of foobar before Lean narrows it to the type of the param?

[Mac]

Yep:

structure Bar :=
  (y : Nat := (fun _ => 1) foobar)

#print Bar.mk
-- constructor Bar.mk.{u_1} : ({x : Sort u_1} → {foobar : x} → Nat) → Bar

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/1320

[James Gallicchio]

Mac said:

One use case of the := is in macros where constructing such a structure can be easier, but I am doubtful that would be a good enough reason to keep the alternative syntax around.

I use it in enough places in my codebase that it would be very annoying if we got rid of it. In particular I have a pattern like

class MyLargeClass (C : Type) where
  field1 : type1
  ...
  fieldn : typen

instance [OtherClass C] : Inhabited (MyLargeClass C) where
  default := {
    field1 := ...
    ...
    fieldn := ...
  }

-- In some other file
instance : MyLargeClass MyType := {
  default with
  field23 := ...
  }

that is pretty nice, and only possible with the := syntax

[Mac]

@James Gallicchio I think the suggestion was just to remove := in structure / class definitions, not elsewhere (e.g., in instance). Thus, I should note that you did not use := in your class MyLargeClass signature. ;)

[James Gallicchio]

Oh, oh, I see now. Reading is hard :)