How does this check exhaustiveness?

I don't think that this is `with` (which is really a series of nested `case` statements with exactly two paths per case).

    case is_email_address?(email) do
      true ->
        case String.length(code) == 6 do
          true ->
            case EmailConfirmations.get_email_confirmation(email) do
              %EmailConfirmation{} ->
                case EmailAddresses.get_email_address(email) do
                  nil ->
                    case Users.create_user(data) do
                      {:ok, user} ->
                        case EmailAddresses.create_email_address(user, email) do
                          {:ok, email_address} ->
                             # success block
                          fail -> fail
                        end
                      fail -> fail
                    end
                  fail -> fail
                end
              fail -> fail
            end
          fail -> fail
        end
      fail ->
        case fail do
          # else conditions
        end
    end

Elixir will be able to do something closer to `case` exhaustiveness checking with the gradual typing being built, and dialyzer can sort of perform exhaustiveness checking as long as your type specs are written well enough. (I’ve observed two things about `with` statements in Elixir: they should have more than one condition clause, or they should be written as `case` statements; they should not have an `else` clause, as that suggests that error path normalization isn't happening at the right level.)

In many ways what's described is much closer to `cond`, except that `cond` is completely open ended except for the required `true` clause, which means that there is absolutely no exhaustiveness checking.

I'll admit that I mostly skimmed this and I don't use ML or Haskell, but I couldn't see what benefit this provides over Elixir's `case` or Rust's `match` (recognizing that the former can't do exhaustiveness checking as yet, but `match` absolutely can).

Just check out the paper's Motivaton section (2).

In ML you can't write something like this:

    if e is
      ...
      Lit(value)
        and Map.find_opt(value) is Some(result)
        then Some(result)
      ...

where the `...` may include many cases and may contain other Lit cases, so that you would need to refactor the whole expression.

Haskell's pattern guards can do this, but they can't "split" control-flow in the middle of a case, as in:

      Lit(value)
        and Map.find_opt(value) is Some(result)
        and computation(result) is
          Left(a)  then ...
          Right(b) then ...

but these all fall out completely naturally in the UCS.

Also, exhaustiveness Just Works without the need of any type annotation. The system is actually type system agnostic.

PS: there's another point being made on Reddit about cond's right-shift problem: https://www.reddit.com/r/ProgrammingLanguages/comments/1g127...

Thank you. I think that I’ll need to read this again with that particular comment in mind, because that makes sense.

The limitations of Elixir syntax means it would need to be something more like:

    ucs do
      expensive() =>
        and cheap1() -> "branch 1",
        and cheap2() -> "branch 2",
      cheap3()       -> "branch 3"
    end

There are other ways around it, but it could be fun to try to build a macro in Elixir for the UCS.

My eyes! They burn!

They should. This nesting is why `with` exists, but even if `cond` and `case` could test for exhaustiveness (they can't currently, and I don't think that `cond` ever could), `with` would not be able to test for exhaustiveness, since there's always two paths described.