Allow trailing commas in the list syntax

[kuruczgy]

• [X] I have read CONTRIBUTING.md.
• [X] I have checked that there is no existing PR/issue about my proposal.

Summary

Trailing commas should be allowed in the list syntax, which is mainly useful when breaking it up into multiple lines.

Motivation

Many languages allow trailing commas. I found this article summarizing the arguments for trailing commas, and their status in various languages.

The two main arguments for me are:

• Diffs. When extending a list, the addition of a new comma on the previous line shows up as an extra modification, adding unnecessary noise to the diff.
• Easy editing. Many editors make it easy to copy, move, delete, etc. lines. With trailing commas, these operations can be used to manipulate the list, without extra effort needed to fix up the commas.

The proposal

When a list gets too long, one usually breaks it up into multiple lines, but extra care has to be taken to break the pattern, and not include a comma for the last item:

[
  foo,
  bar,
  baz,
  quux
]

I would propose to optionally allow an extra comma after the last item as well:

[
  foo,
  bar,
  baz,
  quux,
]

Alternatives considered

Apparently people sometimes use leading commas in Haskell:

  [ foo
  , bar
  , baz
  , quux
  ]

I haven't used Haskell much, so it might be that I am just not used to it, but I still see trailing commas as being superior. (This does not solve either the diff or the editing issue, it just makes it so that the they occur with the first item instead of the last.)

Conclusion

I think we should allow trailing commas anywhere where they don't cause conflicts. The other places where commas are used that I can think of are tuples and bunched arguments.

@Z-snails pointed out on discord that tuples might be problematic though:

idk if it's actually been implemented yet, but tuple sections might conflict with that (ie (x,) is equivalent to \ y => (x, y))

[gallais]

This does not solve either the diff or the editing issue

Leading commas do solve the diff issue.

[kuruczgy]

Leading commas do solve the diff issue.

Care to elaborate? (Again, I am not familiar with the leading comma convention, so I might be just missing something.)

-[ foo
+[ new_item
+, foo
 , bar
 , baz
 , quux
 ]

[gallais]

This diff is no different trailing comma or not as you've modified the line starting with a [.

-[ foo,
+[ new_item,
+ foo,
  bar,
  baz,
  quux,
 ]

[kuruczgy]

Consider the convention where the brackets are on separate lines. With trailing commas, no matter where you add (or remove) an item, the diff will only be a single line. With leading commas, the issue still remains with the first item:

 [
-  foo
+  new_item
+, foo
 , bar
 , baz
 , quux
 ]

EDIT: This is also the way I presented it in my original comment. I don't think I have ever seen the opening bracket being put on the same line as the first item.

[magnostherobot]

I think this would be a nice addition to Idris 2; I feel like I type ddk$x in vim a lot when editing Idris 2 code to delete trailing commas :p

Are there other, similar situations in Idris 2 syntax that would be worth considering alongside lists? All I can think of off the top of my head is that anonymous functions comma-separate their arguments.

Also it might be worth noting that Sirdi uses JSON as its config file format, and JSON does not allow trailing commas.

[ProofOfKeags]

Consider the convention where the brackets are on separate lines.

I have never seen such a convention in the ML family of languages. So this would require retraining people's habits to get it to take properly.

[magnostherobot]

this would require retraining people's habits

The people who are happy without trailing commas would likely be unaffected: they can just do what they've always done. No retraining of habits would be required unless a library using trailing commas became popular and old-schoolers wanted to contribute to it, in which case it's about as difficult to handle as indentation protocols.

I have never seen such a convention in the ML family of languages.

A quick bit of research tells me that not many ML-style languages support trailing commas. Do you think trailing commas aren't supported because people wouldn't use them, or do you think people don't use them because they're not supported? This might be a feedback loop-style scenario where people have never gotten into them because they aren't implemented in the language they're using, and so the feature never gets implemented in future languages.

I think that I personally would benefit from this feature being included in Idris 2, and I don't see a downside to users who are used to the current way of doing things.

[ProofOfKeags]

in which case it's about as difficult to handle as indentation protocols.

For sure. I'm not actually claiming it is a big issue. I was mostly responding to the notion that the convention presented actually exists. By and large in this family of languages it doesn't.

A quick bit of research tells me that not many ML-style languages support trailing commas. Do you think trailing commas aren't supported because people wouldn't use them, or do you think people don't use them because they're not supported?

Definitely the lack of support is what created the leading comma convention. It is not obvious that commas should be leading to just about anyone. They are punctuation in all of the human languages they appear in. However, I think that allowing trailing commas will introduce ambiguity in the source language about what the correct way to do it is. This will matter when source formatters start to show up.

I think that I personally would benefit from this feature being included in Idris 2, and I don't see a downside to users who are used to the current way of doing things.

Maybe. I don't think it's a big deal one way or the other.

[ohad]

You can already use the cons syntax directly:

  foo ::
  bar ::
  baz ::
  quux ::
  Nil