Reduce indentation hell.

[axch]

Implement <- as syntactic sugar for continuation lambdas.

Apply it throughout the prelude to see how it looks. If this is registering as a good change, we can propagate it throughout the rest of the corpus as well.

This fixes #1137 in spirit, if not precisely as filed (i.e., this implements the generalization in the comments, not the original ask).

[axch]

Offline, @dougalm, @apaszke, and I considered changing the syntax further to add a with keyword before the binder, following Koka. We decided against for this PR, but here is a summary of the thoughts:

Option A:

with x <- ...

Pros: A1. Used by Koka (nice as an homage, but since Koka isn't widely used, it probably doesn't matter for users). A2. Better for nullary functions, which can omit the x <-. However, we don't have them yet, and <- ... might work fine too. A3. <- is confusingly close to do notation (but the semantics are close too!) A4. with makes it easier to make it an expression. A5. with highlights that something odd is happening.

Option B: As implemented, i.e.

x <- ...

Pros: B1. Avoids the repeated with weirdness of with x <- with_state foo (though we could rename to start_state or something). B2. Shorter. B3. Binders remain left-aligned as in a sequence of equations.

[axch]

When reading the resulting code, @dougalm and I found that type-changing wrapper functions (most commonly yield_state) get really confusing with the <- notation.

Consider

a = code
b = code
c = code
d <- yield_state something
e = code
f = code
code

You'd think that the return type would be determined by the last line, but it's actually not -- it's determined by the first yield_state that occurs in the block.

However, using with_state the same way is fine --- the only thing that with_state does to the remainder of the block is make a new mutable reference available, and then clean it up when the block exits. But since the return value of the block is forwarded unchanged, those cleanup details are a secondary consideration, and it doesn't feel confusing at all.

We therefore propose a convention, at least for the time being: The <- syntax is for functions that accept a continuation lambda but do not alter its return type; whereas if the return type is changing, use an explicit lambda and indent it.

We considered enforcing this convention with a special type-checking rule, but decided against because (i) that's work, and (ii) it's probably better to see what uses for type-changing <- appear in the wild than to preempt them by making them artificially not work.

[axch]

By the way, with this change Dex can mimic Haskell's do notation:

foo <- action1 `bind`
bar <- action2 `bind`
baz = pure function
action3

Amusingly, this usage adheres to the convention proposed above: bind doesn't change the return type of the continuation lambda. It changes its input type (i.e., f accepts an a but \x. bind x f accepts an m a), and it changes the return value, but the return type stays m b.