Syntax questions

Stream: lean4

[Yuri de Wit]

It seems that it possible to define a ToString instance, for instance, in (at least) two ways:

instance : ToString Rules where
  toString rs := "TBD"

and

instance : ToString Rules := ⟨ fun rs => "TBD" ⟩

But I dont understand the second one: why do I need ⟨ and ⟩ here?

In addition, since it is possible to use {& } to create a structure with named fields, it would be nice to use the same to destructure bindings, but this does not work:

structure Rule where
  (lhs : Term)
  (rhs : Term)

instance : ToString Rules where
  toString { lhs, rhs } := "TBD"

-- or

instance : ToString Rules where
  toString { l := lhs, r := rhs } := "TBD"

I believe this is called record puns in haskell.

Is there a way to do this?

[Henrik Böving]

You need the anonymous constructor Syntax because a class is just a structure and an instance is a value of that structure, if the last thing is already possible in pattern matching im surprised that it doesnt work here yet.

[Yuri de Wit]

The "class is just a structure" makes sense, thanks.

I was also confused about the difference between { & } and ⟨ & ⟩? But it seems that the former is an anonymous constructor to be used with named fields and the latter with positional fields?

And indeed:

instance : ToString Rules := { toString := fun rs => "TBD" }

[Yuri de Wit]

Should I open an issue in Github to add support for this?

structure Rule where
  (lhs : Term)
  (rhs : Term)

instance : ToString Rule where
  toString ⟨ lhs, rhs ⟩ := "TBD"

[Kevin Buzzard]

Isn't the point of Lean 4 that you can write your own syntax yourself to make this happen?

[Kevin Buzzard]

I think the devs are more worried about other things right now

[Yuri de Wit]

Possibly, but I am not sure and that is why I am asking here.

It seems (to me) an inconsistency in the feature set: why support it here but not there (a source of confusion). Besides, creating an enhancement documents the gap and does not mean when or how it is resolved. It could even mean that the enhancement is closed as won't fix (or left there as a need-help), but at least it is documented there as a wont fix

[Kevin Buzzard]

I don't know much at all about Lean 4 but I am interested in the question of whether a user could write this themselves. Do you know? I just have this vague feeling that "you can do anything in Lean 4" but conversely have no understanding at all of these syntax things that people post on this stream.

[Yuri de Wit]

I had a tiny bit of exposure to notation, syntax & macro_rules in Lean4, but only for a completely new notation. I am not entirely sure how to reuse the existing notation but in a different part of the expression tree, though.

[Henrik Böving]

If what comes after where was some syntax category you had access to one could add more ways to do this e.g.

[Henrik Böving]

However in this case this is actually explicitly treated by the compiler as an error, it does recognize the syntax correctly but decide not to elaborate it.

[Henrik Böving]

https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/MutualDef.lean#L164

[Henrik Böving]

I don't know why it's done like this though, note that however:

structure Point where
  x : Nat
  y : Nat

instance : ToString Point where
  toString p :=
    let ⟨x, y⟩ := p
    s!"{x}, {y}"

does work

[Yuri de Wit]

Humm, so tracking down where the compiler does elaborate the anonymous constructor pattern could be part of the solution.

[Henrik Böving]

No I don't think so, the compiler clearly decides in this kind of where based def that it does not want to see a pattern so it will not even attempt to go through with elaboration here.