Kudos to the authors. It takes some fortitude to try to make a contribution to something as fundamental and ubiquitous as the "if" statement. Appreciate providing the grammar and the thorough explanations, will save a lot of pain when trying to implement!
I like that there is this left-to-right flow. I think it’s a bit nicer to read than if-let ordering where the pattern comes before the thing it will be matched against. I think it’s also good for ocaml-style constructor disambiguation, which tends to go in lexical order.
Another nice aspect of making guards a less special case is that it avoids complexities in deciding if a binding is unused. I believe this logic was a source of lots of compiler warning bugs in ocaml.
This syntax doesn’t seem to solve the following problem with matching where there are two paths to the same binding, (say you have an option in one branch but it isn’t optional in the other, and maybe you’d like to handle both cases with the same code. Currently you can do that with a match (match …) with … pattern.
I worry that the semantics around exhaustiveness and mutable values may be confusing, though I guess OCaml already has that problem:
type t = { mutable x : bool }
let n = function true -> 1 | false -> 0
let f t =
match t with
| { x = false } when ( t.x <- true; false) -> -1
| { x } -> n x * 2 + n t.x
What does t { x = false } return? Similarly if you changed the second case to be two cases instead of binding x?
As mentioned in a response to a sibling comment, we plan to support `or`, which should address the problem you mention. (If not, would you have an example of what you mean?)
> I worry that the semantics around exhaustiveness and mutable values may be confusing, though I guess OCaml already has that problem
We added pattern matching and exhaustiveness to Dart not that long ago, and dealing with exhaustiveness and mutability was a big concern since Dart (unlike more strictly functional languages) generally doesn't avoid mutability.
Our solution was that whenever a pattern accesses a property, the language implicitly caches that value. Any future accesses to the same property in that switch statement/expression use the previously cached value. That way, an entire set of switch cases is always operating on an immutable snapshot of data so that exhaustiveness can't be violated by side effects. Spec:
Imagine Left and Right contained data of compatible types, then I'd like to extract that data (regardless of tag) like so:
if x is Left(y) or x is Right(y) then ...
That way I only need to write the `...` part once. (This could be combined with the rest of the pattern matching machinery in interesting ways, and would probably need to have eager matching / short-circuiting semantics in case both cases match).
We definitely want to get into that! Unfortunately it's not completely straightforward. A simple desugaring doesn't work due to our support for intermediate bindings and computations, which we don't want to recompute.
def getNaturalName(tag, globals)
if globals.lookup("0") is Just(Global(_, _, term))
if term is Numeral(_, type, _)
return Just(Name(getTermTag(type)))
error showSyntaxError("0 must be a numeral to use numerals", tag)
return Void
Though this ultimate conditional syntax is more general because lambda zero only allows one destructuring per conditional to simplify parsing.
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).
With traditional matching there are up to five different things:
- if x then y else z. This is roughly like a match with a true and false case but it depends on the language how much that is
- match e with { p -> e }. This is the classic pattern match case
- if let p = e then x. This is roughly equivalent to (match e with p -> x | _ -> ())
- match e with { p when e -> e }. This is matching with a guard but I’ve counted it as a special case because it doesn’t easily designate into a match because of the binding/evaluation order, and the guard is special because it can only go at the top level of the match clause so it isn’t just a special kind of pattern (though maybe it could be)
- let p = e. This is one-case pattern matching used for binding variables or destructuring.
The paper proposes a way to make the first four cases obvious parts of one more unified thing, which makes the language potentially simpler and may reduce some weird warts like where guards can go.
There's such a thing as too high an abstraction. Sometimes 4 different operations really are just 4 different operations and not cases of some mega-construct.
Inspired by duality, I've been trying to work out a language where there's a more obvious correspondence/symmetry between expressions (which evaluate in an environment of named bindings to produce an anonymous value) and patterns (which destructure an anonymous value to produce an environment of named bindings).
In theory, yes: I've used it to derive a (minor but accepted as published) patch to a Turing Award winner's paper; in practice, no.
[the semantics haven't changed much over the past years, but the syntax? even as a single person, who ought to be able to come up with a unified design, my different temporal instantiations insist on bike shedding]
Not the implementation, I think one could do better, but the fact that they identified an interesting opportunity: coming up with the Ultimate Conditional Syntax for pattern matching.
I would love to see them take one more crack at it, and this time try to think about how to reduce the syntax to the bare minimum.
Kudos to the authors. It takes some fortitude to try to make a contribution to something as fundamental and ubiquitous as the "if" statement. Appreciate providing the grammar and the thorough explanations, will save a lot of pain when trying to implement!
I like that there is this left-to-right flow. I think it’s a bit nicer to read than if-let ordering where the pattern comes before the thing it will be matched against. I think it’s also good for ocaml-style constructor disambiguation, which tends to go in lexical order.
Another nice aspect of making guards a less special case is that it avoids complexities in deciding if a binding is unused. I believe this logic was a source of lots of compiler warning bugs in ocaml.
This syntax doesn’t seem to solve the following problem with matching where there are two paths to the same binding, (say you have an option in one branch but it isn’t optional in the other, and maybe you’d like to handle both cases with the same code. Currently you can do that with a match (match …) with … pattern.
I worry that the semantics around exhaustiveness and mutable values may be confusing, though I guess OCaml already has that problem:
What does t { x = false } return? Similarly if you changed the second case to be two cases instead of binding x?As mentioned in a response to a sibling comment, we plan to support `or`, which should address the problem you mention. (If not, would you have an example of what you mean?)
> I worry that the semantics around exhaustiveness and mutable values may be confusing, though I guess OCaml already has that problem
Indeed, and it was until very recently a source of unsoundness: https://icfp24.sigplan.org/details/mlworkshop-2024-papers/8/...
Oh, wow, that's interesting.
We added pattern matching and exhaustiveness to Dart not that long ago, and dealing with exhaustiveness and mutability was a big concern since Dart (unlike more strictly functional languages) generally doesn't avoid mutability.
Our solution was that whenever a pattern accesses a property, the language implicitly caches that value. Any future accesses to the same property in that switch statement/expression use the previously cached value. That way, an entire set of switch cases is always operating on an immutable snapshot of data so that exhaustiveness can't be violated by side effects. Spec:
https://github.com/dart-lang/language/blob/main/accepted/3.0...
The other one I want occassionally is "or".
Imagine Left and Right contained data of compatible types, then I'd like to extract that data (regardless of tag) like so:
That way I only need to write the `...` part once. (This could be combined with the rest of the pattern matching machinery in interesting ways, and would probably need to have eager matching / short-circuiting semantics in case both cases match).We definitely want to get into that! Unfortunately it's not completely straightforward. A simple desugaring doesn't work due to our support for intermediate bindings and computations, which we don't want to recompute.
Looks very similar to lambda zero syntax (https://github.com/clark800/lambda-zero):
Though this ultimate conditional syntax is more general because lambda zero only allows one destructuring per conditional to simplify parsing.Elixir already has this - "with". https://www.openmymind.net/Elixirs-With-Statement/ E.g.:
I don't think that this is `with` (which is really a series of nested `case` statements with exactly two paths per case).
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).
How does this check exhaustiveness?
I don't understand how it's better than traditional pattern matching.
With traditional matching there are up to five different things:
- if x then y else z. This is roughly like a match with a true and false case but it depends on the language how much that is
- match e with { p -> e }. This is the classic pattern match case
- if let p = e then x. This is roughly equivalent to (match e with p -> x | _ -> ())
- match e with { p when e -> e }. This is matching with a guard but I’ve counted it as a special case because it doesn’t easily designate into a match because of the binding/evaluation order, and the guard is special because it can only go at the top level of the match clause so it isn’t just a special kind of pattern (though maybe it could be)
- let p = e. This is one-case pattern matching used for binding variables or destructuring.
The paper proposes a way to make the first four cases obvious parts of one more unified thing, which makes the language potentially simpler and may reduce some weird warts like where guards can go.
There's such a thing as too high an abstraction. Sometimes 4 different operations really are just 4 different operations and not cases of some mega-construct.
I totally agree that can be the case, but I’m not sure it applies that much to the OP.
Inspired by duality, I've been trying to work out a language where there's a more obvious correspondence/symmetry between expressions (which evaluate in an environment of named bindings to produce an anonymous value) and patterns (which destructure an anonymous value to produce an environment of named bindings).
Have you made any progress?
In theory, yes: I've used it to derive a (minor but accepted as published) patch to a Turing Award winner's paper; in practice, no.
[the semantics haven't changed much over the past years, but the syntax? even as a single person, who ought to be able to come up with a unified design, my different temporal instantiations insist on bike shedding]
It looks like it could be more concise sometimes. For instance, you could have this:
The equivalent pattern matching with a match expression in pseudo-ML:I love this.
Not the implementation, I think one could do better, but the fact that they identified an interesting opportunity: coming up with the Ultimate Conditional Syntax for pattern matching.
I would love to see them take one more crack at it, and this time try to think about how to reduce the syntax to the bare minimum.
Here's my read/adding of this language to PLDB: https://www.youtube.com/watch?v=UzsDaq0UdnM