A few weeks^Wmonths ago now, Pierre Dagand asked me about pattern synonyms for OCaml. I told him I had a design conundrum of the worst kind with pattern synonyms: a choice between two incompatible option, with none being better than the other. Synonyms that capture the pattern language, or restricted synonyms that can be used as expressions? Well, it turns out we can have both.

I first heard about pattern synonyms from Conor McBride, when he visited us in Paris for the PhD defense of Nicolas Pouillard. (Maybe there is a reason why I made the next step during a discussion with Pierre?) After Conor mentioned it, it was a painfully obvious idea: our pattern language does not have any form of abstraction! There are difficult and deep problems around ambitious notions of first-class abstraction for patterns, but a let for patterns seems so simple and obvious in retrospect that you’d wonder why nobody has it.

(In a quite appropriate timing, the excellent GHC hackers decided to finally include pattern synonyms just in time for that blog post. Thanks!)

TL;DR for those in a hurry: I suggest that the semantics of a pattern-synonym view as an expression be defined (only) in any branch that matched on said synonym, depending on what has been matched. Read one for more detail.

Pattern synonyms, the easy part

Consider the given AST for a language of boolean tests:

type expr =
  | True | False
  | Var of string
  | Not of expr
  | Or of expr * expr
  | And of expr * expr

The idea is to be able to define, for example:

let-pattern Nand(a, b) = Not(And(a,b))

and then in a pattern matching, use them as patterns:

| Nand (a, b) -> Or(Not a, Not b)

Mild troubles

Of course, when someone proposes a feature, the first thought of any language designer is to shoot it down by explaining what terrible, terrible problems it creates.

The obvious issue with pattern synonyms is: don’t they break abstraction? How would you compile a pattern whose definition is hidden/abstracted by a module interface? Won’t that break the efficiency of pattern-matching compilation? What about the exhaustivity check? (In Haskell, do we know the strictness of the pattern arguments?)

Those are indeed problematic questions that F#’s Active Patterns, for example, had to handle – as a much more expressive way to inject unknown patterns. (Maybe we are too hung up on the efficient gains of pattern-matching compilation. But I think that exhaustiveness checking is of mighty importance, and the Haskell community unfortunately tends to overlook it.) Luckily, we don’t have to solve them; we can just say that the interface of a pattern-synonym is its definition. No actual abstraction, compilation as usual.

Maybe we can refine this later, but it’s ok to restrict ourselves to the simplest feature possible.

Are patterns expression?

During that chat in a Cambodian restaurant (check out the Gagallium recommendations for Asian restaurant in Paris, soon to be released), Conor mentioned that you could also use a pattern synonym on the right-hand-side:

let f x = Nand(x, x)

Pattern-synonyms are necessarily linear in their variables, as the following would not be valid in a pattern-matching:

let-pattern Wrong x = Nand(x, x)

But that doesn’t stop them from being used as expressions. There could be an issue with universal patterns:

let-pattern Foo(x) = Nand(_, x)

But forbidding Foo (as it cannot be used as an expression) does not restrict expressivity: just use the version with a variable instead (Nand), and pass a _ at the point of use.

There is however a problem with or-patterns (which OCaml supports):

let-pattern Op(a,b) = (And(a,b) | Or(a,b))

Those definitely do not make sense as expressions. Horror, we have a choice to make: should we support pattern synonyms only the patterns that are also embeddable as expressions, or rather support the full pattern language?

There are partisans for either choice, but none definitely more convincing than the other. Of course, there is the option to capture the full pattern language, but only allow on the right-hand-side those that also are expressions. It still feels a bit ad-hoc.

Tadaam

Watch this:

let-pattern Op(a,b) = (And(a,b) | Or(a,b))

let rec map f = function
| (True | False | Var _) as t -> t
| Not a -> Not (map f a)
| Op (a, b) -> Op (map f a, map f b)

The Op line makes perfect sense, right? I claimed that Op does not mean anything on the right-hand side, but here it clearly does, in the sense that anyone seeing those lines of code understands what it does: Op on the right means “the same thing that was matched on the left”: if it was And, it’s And, and if it was Or it’s Or.

More precisely, a pattern matches a certain number of head constructors of the data in the scrutinee, ie., a context (data context, this is not about control operators). When a pattern-synonym matches a given context C[x,y...], it is bound in the corresponding right-hand side of this context viewed as an expression, that is the function fun (x,y...) -> C[x,y...]. This semantics covers the whole pattern language – I’m not sure about view patterns, but we don’t have those in OCaml.

Universal patterns and or-patterns are in fact the only construction such that the matched context varies at runtime (according to the branch chosen); in other cases (I will call those “deterministic” patterns), the simple fact that it matched suffices to determine the matched context (which is why they would also make sense as an expression independently of any pattern-matching).

Note that I’m cheating a bit. I said we could use pattern synonyms as expressions, but added a restriction: only in a branch of a pattern-matching that used this synonym. This is less flexible that the “use it anywhere” possible with deterministic patterns. We could ask for both features: deterministic patterns as expressions anywhere, plus general synonyms as expressions under a capture.

Troubles

François, who is an expert in shooting down lousy ideas, immediately pointed out a problematic case:

match t1, t2 with
| ...
| Op(a, b), Op (c,d) -> Op (f a b, g c d)

What would Op mean here? My answer is that Op in a right-hand side should be considered bound by the pattern, just like variables are, and that this is invalid just as (x, x) is an invalid non-linear pattern. But you would still like to allow people to repeat Op on the left, so it’s tempting to forbid non-linear patterns only when the variable is actually used (as we do in case of ambiguous name shadowing). Or maybe you could expect non-linear uses to do an equality/unifiability check, but that’s an orthogonal issue I won’t go into.

(What about (Op as f)(a, b) as a way to bind the context-fragment to f and use it non-ambiguously? Head-context capture will triumph.)

My point is: complainers are gonna complain, but I think this idea stands as a cohesive unit, and has the merit of resolving a tension between two interpretations of pattern-synonyms that I didn’t know how to solve before.

This idea is so natural that I expect someone to have come up with it before, but I’m not aware of it and it’s hard to search, so please tell us if you know about it!

Post scriptum: formalization

I wrote a precise semantics for this idea on my whiteboard, but am too lazy to write them down. Or rather, the problem is that as soon I do LaTeX, I get tempted to add ten new orthogonal ideas about patterns. The core idea is that the semantics of a pattern is a set of (context, substitution) pairs. If you want to be operational, you can instead turn each (scrutinee, pattern) pair into a either (context, substitution) pair or a match failure. In contrast, previous formalization (eg. Focusing on Pattern Matching, by Neelakantan Krishnaswami, 2009) generally only care about the substitution, and the matched context is not made explicit.

Update (01/27)

Arnaud Spiwack promptly found an interesting counter-example where this idea does not suffices to express all patterns as expressions:

let-pattern FooBar(x, y) = Foo ((Bar x) as y)

(Dear haskell reader: as is the equivalent of your @-patterns.)

The claim must be revised: we still cannot express all patterns as expressions, but we can solve the part of the problem that is due to disjunctive patterns and/or universals. This use of as, or more generally pattern intersection, creates interferences between distinct bound variables – reminding of how implicit relation between type variables make variance for GADTs difficult.