Dhall-lang: [RFC] Syntax: Shorthand lambda

[hanshoglund]

This is a proposal to allow the syntax λ(x1 : T1) (x2: T2) (xN : TN) -> e as a shorthand for λ(x1 : T1) -> λ(x2 : T2) -> λ(xN : TN) -> e.

[Gabriel439]

I have few clarifying questions:

• What about a more compact style where the arguments were comma-separated, like this:

  λ(x1 : T1, x2 : T2, …, xN : TN) → e
  

  That way the syntax would more greatly resemble the syntax for a record?

• Would an empty list of bindings be legal? (i.e. λ → e)

• Would this also include a similar syntax for function types (i.e. ∀(x1 : T1) (x2 : T2) … (xN : TN) → …)?

[ari-becker]

@Gabriel439

* What about a more compact style where the arguments were comma-separated, like this:
  ```haskell
  λ(x1 : T1, x2 : T2, …, xN : TN) → e
  ```


  That way the syntax would more greatly resemble the syntax for a record?

Recall that λ(x1 : T1) → λ(x2 : T2) → is not the same as λ(x2 : T2) → λ(x1 : T1) →. If the syntax resembles a record, it may confuse the user into thinking that the order of arguments is immaterial, like how the order of fields in a record is immaterial.

[Gabriel439]

@ari-becker: So there is a related feature that has been requested a couple of times, which is "dependent records" (i.e. ordered records, where one field's type can depend on the value of a prior field). If we were to come up with a syntax for dependent records then we could reuse that syntax for ordered function arguments.

For example, suppose that the syntax for a dependent record used semi-colons to separate key-value pairs, like this:

{ x = v1; y = v2; … }

... then we could use that same separator for compressed function arguments, too:

λ(x1 : T1; x2 : T2; …; xN : TN) → e

[hanshoglund]

Upon reflection I'd like to withdraw this proposal.

Minor syntactic changes are likely to distract maintainers from more urgent work on implementation/performance.