Trailing comma for lists

Stream: lean4

[Leni Aniva]

Would it make sense to create an RFC to allow lists to have a trailing comma? For example, this is not legal Lean 4:

let li = [
  item1,
  item2,
]

but if it were legal, adding new elements would not require modifications to existing lines:

let li = [
  item1,
  item2,
  item3,
  item4,
]

Using a trailing comma is supported in many languages and simplifies diff generation and automatic code generation.

I encountered an use case for it while writing unit tests.

[James Gallicchio]

FWIW, I actually feel less need for trailing commas in lean than other langs. If you're doing auto code generation, and you're using Lean's metaprogramming stuff, the $[ whatever ],* combinator just does the right thing, which is really helpful.

That said, I'm very much not opposed to this :) if core devs felt particularly wild, I'd even ask for leading commas, so I can write my preferred list syntax of

let list := [
  , item1
  , item2
]

which is, of course, controversial, but every functional programmer has their quirks...

[James Gallicchio]

or, even more out there, maybe we re-visit bulleted lists and provide bulleted list syntax for list literals, which I would very much like.

[Mario Carneiro]

lean has built-in support for optional trailing commas with the (p),*,? syntax, we just need to use it more in the grammar

[Mario Carneiro]

I think the pattern match should still Just Work in that case

[Leni Aniva]

Mario Carneiro said:

lean has built-in support for optional trailing commas with the (p),*,? syntax, we just need to use it more in the grammar

can you give an example of this? edit: nvm found it

[Leni Aniva]

James Gallicchio said:

FWIW, I actually feel less need for trailing commas in lean than other langs. If you're doing auto code generation, and you're using Lean's metaprogramming stuff, the $[ whatever ],* combinator just does the right thing, which is really helpful.

That said, I'm very much not opposed to this :) if core devs felt particularly wild, I'd even ask for leading commas, so I can write my preferred list syntax of

let list := [
  , item1
  , item2
]

which is, of course, controversial, but every functional programmer has their quirks...

I've only seen this style in C++ initializer lists where the first separator is decreed to be :

[Leni Aniva]

RFC: https://github.com/leanprover/lean4/issues/2635

[Ioannis Konstantoulas]

I have read the leading comma referred to as "Haskell-style", and so assumed it is used in Haskell code bases, but I have no clue.

[Joachim Breitner]

Haskell allows neither leading nor trailing comma, so a common style there is

let list :=
  [ item1
  , item2
  ]

[Mario Carneiro]

the leading comma thing looks like a trick people invented to make the no trailing comma issue more palatable

[Leni Aniva]

Joachim Breitner said:

Haskell allows neither leading nor trailing comma, so a common style there is

let list :=
  [ item1
  , item2
  ]

This is the style some people use to write C++ initializer lists so new fields don't mess up the diff

[Leni Aniva]

https://github.com/leanprover/lean4/pull/2643
I got it working for everything except for arrays. The analogous change to arrays breaks deriving ToJson for some reason