let ... else syntax in progn let ?

[gefjon]

I'm unsure of the status of the Rust proposal on this one, but now that we have pattern exhaustiveness checking, it would be nice to have a way to write non-exhaustive destructuring without rightward drift in progn let, like:

(declare truly-head (List :a -> :a))
(define (truly-head im-sure-this-is-a-cons)
  (let (Cons hd _) = im-sure-this-is-a-cons))
  hd)

It seems reasonable (although honestly, not my first choice) to disallow the above in favor of requiring a version that explicitly handles the Nil case. But using match in this case (or, really, in more complicated but similar cases) leads to undesirable visual noise and rightward drift. Consider:

(declare long-function-that-uses-head (List :a -> :b))
(define (long-function-that-uses-head im-sure-this-is-a-cons)
  (match im-sure-this-is-a-cons
    ((Cons hd _)
      ;; imagine several lines here
     thing
     )
     ;; so that this next part is far-removed from its parent `match` statement
     (_ (unreachable))))

Or, a similar version that retuns an None instead of signaling an error:

(declare long-function-that-returns-opt (List :a -> Optional :b))
(define (long-function-that-returns-opt im-sure-this-is-a-cons)
  (match im-sure-this-is-a-cons
    ((Cons hd _)
      ;; imagine several lines here
     (Some thing)
     )
     ;; so that this next part is far-removed from its parent `match` statement
     (_ None)))

Instead, I propose copying Rust's let ... else construct, to rewrite the above as:

(declare long-function-that-uses-head (List :a -> :b))
(define (long-function-that-uses-head im-sure-this-is-a-cons)
  (let (Cons hd _) = im-sure-this-is-a-cons else (unreachable))
  ;; imagine several lines here
  thing)

(declare long-function-that-returns-opt (List :a -> Optional :b))
(define (long-function-that-returns-opt im-sure-this-is-a-cons)
  (let (Cons hd _) = im-sure-this-is-a-cons else (return None))
  ;; imagine several lines here
  (Some thing))

Notice how the let else version keeps the handler for the failed-match branch close to the match itself, where the match version has the handler for the failed-match branch somewhat removed from its source; and how the let else version avoids rightward drift.

The semantics should be:

• progn let bindings without an else clause must be exhaustive.
• progn let bindings with an else clause need not be exhaustive.
• The else clause of a progn let must not return normally.
  • In Rust terms, its type must be !.
  • In Haskell terms, its type must be forall a. a.

In my mind, the main obstacle here is whether we can check that a form doesn't return. Is that feasible?

As always, I am not particularly attached to this specific syntax, so long as whatever we decide on doesn't introduce any nesting of subsequent/body forms.

[eliaslfox]

I think extending the type system to support this will be difficult.

Rust's never type being first class seems like it has some issues (I just glanced over rust-lang/rust#35121).

Coalton doesn't have rank N types, so forall a. a isn't really something we can check for. We theoretically could try to check if a type is forall. a but i'd like to avoid that. Also because of #84 it's easy to accidentally get forall. a types.

[eliaslfox]

That being said, I think let ... else and other syntax sugar to reduce nesting would be really nice. An easier first step would could be to introduce something like Rust's if let ... else.