Ergonomics of end markers

I’m glad you brought up Lean4!

I really like the syntax of Scala3 and Lean4 with their respective minimal end-marker syntax requirements.

End markers should be required only when indentation cannot convey a syntactic change of scope. Elsewhere, end markers should be optional to help minimize syntactic noise.

Although Lean4 namespaces are analogous to Scala3 objects, Lean4 does not require indentation of nested namespaces, e.g., the following is OK:

namespace A
-- definitions in A
namespace B
-- definitions in B
end B
end A

The point here is that namespace end markers are required in Lean4 to unambiguously convey an important change of syntactic scope.

For Scala3, since a nested object must have a higher indentation than its parent scope, the object end marker should be optional.

  • Nicolas.
1 Like

Having used both Scala 2 and Python extensively in recent years, I like the optional braces in Scala 3. However, the introduction of end markers feels strange. A few points:

  1. What is their purpose?
    1. Readable vs cluttered code:
      1. Optional braces is very clean syntax.
      2. end def longwindedlyNamedMethod is not clean, but is quite clear in a verbose, literal sense.
    2. Copy-paste safety: only available with always mandatory end markers, so not achieved regardless.
  2. Can we rely on the IDE / code editor?
    1. Editing braces is still a pain in most editors, even though it “shouldn’t” be - do developers in general actually remember whatever the hotkeys are for inserting/deleting them in a paired fashion? I sure don’t. So optional braces definitely add something.
    2. Can “end marker style information” be provided by the IDE instead of the developer?
      1. Yes, but it’s of course somewhat subjective precisely when to provide it, so there will be bikeshedding.
      2. Yes, but they currently don’t, and we can type end def longwindedlyNamedMethod today.
    3. If it can’t, aren’t we on some level assuming a “simple” editor? And simple editor + end def longwindedlyNamedMethod => additional renaming pain?

My conclusions from the discussion and points above:

  1. Do use braceless style, but generally avoid end markers.
    1. Only seriously consider them in case b, when the closing definition is longer than ~20 lines.
    2. My preferred mode would be that I write end and then the IDE automatically appends a live comment with the full first line of the closed statement. That allows keeping the actual code to an absolute minimum, while providing the key information on an as-needed / as-requested basis.
  2. Ichoran’s end [def] [xyz] proposal looks good.
  3. Linters etc should not nag about omitted end markers in any case, but may want to nag about missing type/name specifier information for them.
1 Like