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
)
```