Allow omitting 'in' in chained bindings

[vapourismo]

In my head this is a purely cosmetic change.
It should not change the validity of programs that are currently valid.

What was previously written as

   let l = λ(n : Natural) → λ(m : Natural) → λ(x : Natural) → n + m * x
in let f = l 2 3
in f 445

can now be written like

let l = λ(n : Natural) → λ(m : Natural) → λ(x : Natural) → n + m * x
let f = l 2 3
in
    f 445

This effectively makes in terminate a let-chain.

---

PR: dhall-lang/dhall-haskell#662
Related: #226

[f-f]

Partially referencing the discussion in dhall-lang/dhall-haskell#662 and continuing from there:

I have to say that this proposal is intriguing, because:

• it is not framed as a "desugaring" proposal (as Syntactic sugar for multiple lets and lambdas. #226 was), but it's a change to the single way of doing this
• as @vapourismo already mentioned in Allow omitting 'in' in chained bindings dhall-haskell#662 (comment), it actually addresses a syntax pain point, getting rid of a significant amount of "superfluous" chars (I can compare this feeling to the [] : Optional → None change).
  In fact, a common issue I encounter with refactoring let bindings is that adding a new let clause before the first one needs also an additional in in the previously-first-now-second line (additional point: this messes up diffs).
  With this change one could instead shuffle lets around freely.

So I guess I consider this a good idea, but there is a big downside we should carefully consider: this is going to break basically all the existing expressions

[vapourismo]

From what I gather, this won't break expressions.
The let which previously was in let, is not a residual of the expression in the previous binding. Instead it comes after the expression in the same way the in does. However, it does complicate things for an unfamiliar reader if the code is not properly indented.
I haven't had much time to investigate this further, I may be completely wrong.

I am not sure if the reshuffling is a good idea. It certainly complicates implementations as they now have to track dependencies between the bindings. The top-to-bottom order is fool-proof both for readers and implementation.

[f-f]

@vapourismo oh sorry you're right, this won't break anything 👍

Re: reshuffling: I wasn't talking about implementations doing it, but about programmers (me in this case) refactoring code. Example:

Let's say you have this program:

let b = 2
in b

Now if I want to add an a before b, I'd need to also change the line with b:

let a = 1
in let b = 2
in b

However, with your proposal, I could just add a line before that without changing anything else:

let a = 1
let b = 2
in b

and this is nice 👍

[vapourismo]

Ah, I misunderstood.

[Gabriella439]

I'm still weakly opposed to this, but I must relent if @f-f supports it 🙂

Continuing the discussion from dhall-lang/dhall-haskell#662, what I mean by "significant" code compression is that it changes the "code complexity" (i.e. Big-O code size). This is only a constant-factor improvement, which is why I'm reluctant to add it given that it introduces yet another way to express the same idea.

Probably the easiest way to explain "code complexity" is by comparison to the constructors keyword. The amount of code necessary to produce the equivalent record of alternatives without the constructors keyword is O(N^2), where N is the number of union alternatives. The size of the code with the constructors it is O(N) (and you can reuse the original union type which you probably already have lying around anyway).

Similarly, any feature which removes unnecessary type annotations (like Some) is an improvement to code complexity because there is no upper bound on how large a type annotation could potentially be (and we see many huge types in the wild for Dhall's use case of complex configuration files).

The reason I try to minimize having multiple ways to express the same thing is due to my experiences teaching Haskell. I discovered that many Haskell learners were routinely surprised by many basic equivalences like:

• f x y = z being equivalent to f = \x y -> z
• \x y -> z being equivalent to \x -> \y -> z
• Pattern matching and if expressions being syntactic sugar for case
• (+ 1) being equivalent to \x -> x + 1

Every time you add such a new equivalence the learner typically asks why the language has two ways to express the same idea. In particular, they often ask if one version behaves differently. For example, in the context of let expressions the obvious questions that beginners might ask are:

• Can multi-let expressions be reordered? (No)
• Do multi-let expressions permit mutual recursion? (No)

Whereas if you express expressions as nested let-in expressions then the answer to both of the above questions is unambiguous because the scope of let-bound variables is clear.

[jneira]

I agree with @Gabriel439 here and continue thinking that records could be an alternative although you have to group the variables in dependency levels, making it clear:

let lvl1 = { a = ..., b =... }
in let lvl2 = {c = using a, d = using b, e = using a and b, ... }
in

In case of choose remove the in part, i would go for remove the intermediate let too:

let a = .... , b = .... , c = ....
in 

[jneira]

Thinking in the record alternative, it is clear that it would need record matching as suggested by @ocharles in #226 (comment)
I would be happy to make explicit the dependency levels without prefix (although in the worst case you will end with a let .. in for each variable):

   let { a, b } = { a = ..., b =... }
in let { c, d, e, ... } = {c = using a, d = using b, e = using a and b, ... }

Is not useful to know that the variable definition must be in a block that is above the current one?

[vapourismo]

@Gabriel439
I completely understand that introducing multiple ways to accomplish the same is a bad thing to do. We've learned this from plenty of other languages. However, in this case the difference between the two options (ignoring lambdas) is so tiny and the benefit to my eyes is incredible.

It's funny that you list specifically these two questions from learners. They are exactly two of the ones that I had when starting with Dhall. In fact, I initially believed in let is just a syntactical chaining construct. The way examples were formated didn't make this obvious. Only after digging into the parser did I realize that my belief is completely absurd.

I've made the observation that the current status quo of formating bindings is very annoying to a beginner. I eventually forfeited to it. Maybe this can be improved.

@jneira
This aims to clean up big let-in chains. In most cases a binding in the bottom depends on an earlier binding. Records can't be used for this, yet.

[jneira]

@vapourismo mmm, i meant that you can use several records for that, grouping the variables. A runnable example would be:

    let x =
        { a = 1
        , b = 2
        }
in  let y =
        { c = x.a + 1
        , d = x.b + 2
        , e = x.a + x.b
        }
in  let z =
        { f = x.a + y.e
        }
in  z.f

You save three in let in this case (instead six in) and you have to use the prefixes in exchange, with record matching (not supported yet) it would be:

    let { a , b } =
        { a = 1
        , b = 2
        }
in  let { c , d , e } =
        { c = a + 1
        , d = b + 2
        , e = a + b
        }
in  let { f } =
        { f = a + e }
in  f

Obviously you start to save chars only from 10/15 vars.

[Profpatsch]

and the benefit to my eyes is incredible

To be honest, I don’t see any benefit at all, apart from confusion, especially concerning the very important question whether let statements are self-recursive. If you remove the chain of in, it’s not apparent from the syntax anymore, and the semantics has to be conveyed (and remembered) by some other means.

[Gabriella439]

In the interest of avoiding hostility I'm going to ask that people refrain from using GitHub reactions (both positive and negative) to weigh in on a divided issue like this one since they can easily be misconstrued and turn this into a popularity contest instead of a technical discussion.

GitHub reactions also don't factor into whether or not to accept the proposal. Proposals are approved according to the rules outlined here:

• https://github.com/dhall-lang/dhall-lang/blob/master/.github/CONTRIBUTING.md#how-do-changes-get-approved

To summarize those rules inline here:

• Two people currently get a vote on proposals (me and @f-f)
• In the event of a tie the proposal is accepted
• The absence of a vote counts as an affirmative vote
• Voting deadline is 7 days after proposal submission

I've already indicated that I plan to vote against the proposal, but if the proposal is accepted I will still embrace it wholeheartedly. The main thing we need is an explicit vote from @f-f. The more quickly we make a decision, in either direction, the more likely we can avoid conflict.

No matter which way we decide there will be people unhappy with the outcome, but agreeing to our shared rules and embracing their outcome is vital to sustaining the project's long-term health.

[joneshf]

That response seems like the sort of thing that might end up in a code of conduct. I don't want to derail the issue, but maybe keep that response in the back of your mind until the time comes.

[vapourismo]

Cool, thank you for considering.

[f-f]

It looks to me that this point about "making let better" comes up often lately, so it's worth thinking hard if we can do something about it.

Recapping the ideas around so far:

• omit in in chained bindings (this proposal)
• omit let in in chained bindings (Syntactic sugar for multiple lets and lambdas. #226)
• using records instead, if record matching is introduced (here and in Syntactic sugar for multiple lets and lambdas. #226)

While we try to improve the experience in some aspect we should make sure not to make some other aspect worse - in particular the point about having "one way to do things" is really important to keep in mind (the danger is to mess up things like beginners experience).
We consistently applied this reasoning when discussing other proposals already, such as #226 and #220 (and some others). Now, it doesn't mean that since we applied it some times already we necessarily have to continue doing it, but ensuring consistency in this regard is important for the language evolution (and here I mean the "slippery slope" pattern).

I consider this "almost another way to do things": it technically is, but it doesn't feel like it.
Additionally it scratches a personal itch (messing up diffs) so I'm weakly in favor of this change.

As Gabriel recapped above, in the event of a tie on a proposal then it goes through.
However in my personal value system I strongly prefer "reaching unanimity through discussion" vs "achieving a majority through voting". So I guess I should propose to change the rules to approve proposals to have stronger majority or unanimity - however I'm not sure how well it would scale once we have more votes. Moreover, as we see in this case, there's always the possibility to apply some flexibility in the judgement.

So since there's no unanimous consensus on this (unlike there was for other language changes, like #138 or #227), I propose we should:

• hold off on this proposal for a while
• run a poll around users to see how big of a pain point this is
• collect some more ideas and explore a bit more the solution space

(@Gabriel439 this effectively counts as a negative vote)

[FintanH]

For me it's mostly aesthetic and most minor of pains having to add an in where there wasn't one before or forgetting to add them at all.

I would prefer what was proposed in #226 i.e.

let foo = ./foo
    bar = ./bar
in foo bar

I am starting to take up the habit of binding all imports at the top of the file due to the freeze hashes wrecking havock on diffs 😄 so less ins would be nice. But again, it's mostly aesthetic.

[ocharles]

#226's proposal (for let) is a familiar approach, too. Haskell does this (when you're not in do), as does Nix.

It may be productive to come up with a concrete set of proposals and work through them one at a time, so we're all clear which are rejected (and why), and which are still on the table.

[Gabriella439]

Alright, then I'll change my vote to approve this, but I would still prefer to require a let in between definitions (i.e. this proposal). I would like to avoid using only newlines to separate definitions because:

• (A) then the language is no longer newline-insensitive
• (B) then we would need to use indentation to detect the end of a definition spanning multiple lines, which specifying and parsing the grammar more difficult and makes the language indentation-sensitive

[FintanH]

@Gabriel439: So to clarify the style would be:

let foo = ./foo
let bar = ./bar
in foo bar

correct?

[Gabriella439]

@FintanH: Correct

Also, how the Haskell implementation would format things is technically outside of the scope of this proposal since it's not a standardized behavior, but I assume that the Haskell formatter would now format the expressions like this:

let foo = 1
let bar = 2
in  foo + bar

In other words, one space after let and two spaces after do so that the definitions and the body of the let expression are aligned.

[jneira]

Alright, then I'll change my vote to approve this, but I would still prefer to require a let in between definitions (i.e. this proposal).

And what about use commas (or another single char) to separate them (as suggested in #260 (comment))?

let a = 1, b = 2
in  a + b

The formatting could be

let foo = 1
  , bar = 2
  , baz = 3
in foo + bar + baz

[Gabriella439]

@jneira: Yeah, I would be okay with commas, too, because it looks similar to defining the fields of a record and looks nicer when defined on one line

@vapourismo: What do you think about using , as a separator?

[f-f]

@Gabriel439 @jneira using commas would not solve the problem of shuffling bindings around

Example: if I have

let foo = 1
  , bar = 2
in  foo + bar

I cannot just cut the line with bar and move it above foo without retyping both of the lines, while having only let would avoid this issue

[FintanH]

Ya @f-f has a strong point there 👍

[kedashoe]

If dhall were to allow leading commas, we would avoid the shuffling problem and could also fix #66 with the same convention

let
  , foo = 1
  , bar = 2
in  foo + bar

colors = [
  , "Red"
  , "Blue"
  , "Green"
  ]

[vapourismo]

I prefer the let to a comma, mostly due to the more organic alignment and conflict free reordering that @f-f mentioned.

It is worth noting that the perceived grammar would be simpler with commas, as they are also used in records to seperate label '=' expression.

[jneira]

Mmm, but only the first one, right? Usually you have more than two vars and i am not sure if being able to move a var to the top without retyping is better than the save in chars and the more clear aspect (that one is totally subjective of course)
My dhall files usually have in top one o more imports:

let prelude = /path/to/prelude
  , types = /path/to/types
  , var1 = value1
  , var2 = value2
...

And it is no very frequent to move other binding at the top to replace prelude but, hey, i guess there are other files structures.

Anyway i dont want to extend the discussion further and fall in the wadler's law so simply go ahead with it 😄

[Gabriella439]

Yeah, I think we should just go with leading lets instead of commas for now. We can always add support for commas later