Hello Discourse,
I thought it might be amusing to share two ideas for extending OCaml’s pattern-matching syntax. (I don’t plan to implement them for now because technically it would be difficult.)
with-patterns using and
Agda has with abstractions, which allow to start, in the middle of a pattern-matching, to further match on the value of an expression:
filter_map : {A B : Set} → (A → Maybe B) → List A → List B
filter_map f [] = []
filter f (x ∷ xs) with f x
filter f (x ∷ xs) | Some y = y ∷ filter_map f xs
filter f (x ∷ xs) | Nothing = filter_map f xs
The experimental with-patterns extensions of the ocaml-patterns project had a restrict proposal of “with patterns”: pattern with pattern = expression
let rec filter_map f li =
match li with
| [] -> []
| x :: xs with Some y = f x -> y :: filter_map f xs
| x :: xs with None = f x -> filter_map f xs
Personally, I’m not fond of the use of with in this position, because in match .. with the with keyword sits between the expression and the handler. So I would propose to use and <expr> with <pat> instead of with <path> = <expr>:
let rec filter_map f li =
match li with
| [] -> []
| x :: xs and (f x with Some y) -> y :: filter_map f xs
| x :: xs and (f x with None) -> filter_map f xs
“match li with x :: xs and f x with Some y” actually sounds nice.
Note: one could think of and as a natural keyword for “pattern intersction”, a feature that of course should exist in OCaml, but we don’t need to reserve it for this usage as we already have a pattern-intersection keyword, namely as: p as q is the pattern that matches values that match both p and q, and experts in the environment the pattern variable bound in both p and q.
Note: with-patterns generalize Haskell’s view-patterns (<expr> -> <pat> as a pattern matching on a foo when the expression is a conversion function of type foo -> bar and the sub-pattern matches on a bar) by defining f -> p as syntactic sugar for x and (f x with p) for a fresh x.
Note: this does not give you all the power of Agda with-patterns, as you cannot share the matching context (the patterns on the original expressions) and return different right-hand-side based on the new expression only, forcing you to duplicate more code. But this is solved the next proposal!
Generalized handlers
The current OCaml grammar for pattern-matching is of the form match <expr> with <handler>, or function <handler>, where <handler> is a list of clauses
<pattern> [when <expr>] -> (<expr> | .)
The idea of “generalized handlers” is to allow handlers to be nested inside patterns instead of begin only at the toplevel. For example, the following are equivalent:
match e with
| (p, q1) -> e1
| (p, q2) -> e2
match e with
| (p, (q1 -> e1 | q2 -> e2))
In the second example, the handler is inside a (p, _) pattern (which does not itself have a -> ... right-hand-side). The scoping environment of the expressions inside a nested handler contains all the pattern variables that are defined in the pattern context around them – including some that are visually “to the right” of the expression. For example, the following would be (dubious but) legal:
let negate : sign * int -> int = function
| ((Neg -> -x | Pos -> x), x)
Finally, generalized handlers combine with and-clauses (by the simple rule that handlers are allowed whenever a pattern was allowed before) to provide Agda-style with-abstraction:
let rec filter_map f li = match li with
| [] -> []
| x :: xs and f x with (
| Some y -> y :: filter_map f xs
| None -> filter_map f xs
)