The Algebra of Patterns

The main contribution of this work is to support a rich catalog of equivalences for patterns. In fact, we strive to treat patterns as a boolean algebra which consists of negation patterns, and-patterns, or-patterns, wildcard-patterns and absurd-patterns, featuring all the expected equivalences. This is challenging from the perspective of variable binding. For instance, we want the law of double negation, i.e. $⟦\neg \neg p⟧\equiv ⟦p⟧$, to hold, but this entails that we cannot ignore variables that occur inside patterns in a negated context. We will demonstrate that we can achieve the desired equivalences by a variable binding definition that tracks whether variables occur under an even or odd number of negations. A related problem is to have well-defined variable binding in the context of or-patterns $p\parallel p^{\prime }$, which requires a careful definition of linearity to make sure that the same variables are bound in all cases of an or-pattern. We also describe the conditions under which we can replace a pattern $p_1\parallel p_2$ by the pattern $p_2\parallel p_1$; this transformation is not semantic preserving in most systems which implement or-patterns.

The rest of this article is structured as follows:

• $\mathrm{■}$

  In Section 2 we motivate why the first-match semantics that most programming languages use for pattern matching fails to address several important reasoning and software engineering problems. We show how our contributions can improve upon this status quo.

• $\mathrm{■}$

  In Section 3 we present our first main contribution: the algebra of patterns. We describe the syntax of patterns, the rules for non-deterministically matching a pattern against a value, and the restrictions that characterize the subset of linear and deterministic patterns. We also prove the algebraic properties that characterize the semantic equivalence relation on patterns.

• $\mathrm{■}$

  Section 4 introduces our second contribution, a small term language that contains pattern-matching expressions with default clauses. This section also introduces exemplary typing rules to the untyped patterns of Section 3 and the constructs of our term language; the compilation of patterns described in later sections, however, does not depend on patterns being typed.

• $\mathrm{■}$

  Not all extensions to pattern matching can be compiled to efficient code, but ours can. In Section 5 we show how to compile patterns by translating them to a variant of a disjunctive normal form. We use these normalized patterns in the compilation of pattern-matching expressions to decision trees, which we describe in Section 6.

• $\mathrm{■}$

  We discuss future work in Section 7, related work in Section 8 and conclude in Section 9.

The results in sections Section 3 have been formally verified in the proof assistant Rocq, and are made available as complementary material. Theorems and definitions which have been formalized are marked with the symbol .

Equational reasoning is one of the most important methods functional programmers use to reason about code. Equational reasoning allows us to show that two expressions are equivalent if we can obtain one from the other by a series of rewriting steps. Each rewriting step is justified by some equation between terms, and functions defined by pattern matching are one of the main sources of such equations. Take, for example, the definitions of the functions “id” and “map”:

We can show that mapping the identity function over a list returns the original list, i.e. that $\text{map}(\text{id},xs)=xs$ holds, by using the individual clauses of the definition of “map”:

We have annotated each rewriting step with the equation that justifies it, and in the last step, we have used the induction hypothesis (IH). In this example, we have used the fact that every clause of the pattern match is a valid equation that we can use for rewriting. But this was only valid because the equations in the definition of “map” do not overlap. To see why this is essential, consider the example from the introduction again:

If we are using these clauses as equations we can now show that True is equal to False, using the proof $\mathrm{𝚃𝚛𝚞𝚎}{=}_{(4)}\text{isRed}(\mathrm{𝚁𝚎𝚍}){=}_{(5)}\mathrm{𝙵𝚊𝚕𝚜𝚎}$. A human is of course very unlikely to make such a silly mistake, but if we cannot guarantee that every clause holds as a valid equality between expressions, then we also limit what automatic tools can do for us.

Software engineering has been described as the problem of integrating programming over time [27]. This means that we not only have to understand the meaning of a program at a fixed point in time, but we also have to understand how the meaning of a program changes as it is developed and maintained. It should therefore be as simple as possible to reason about how the meaning of a program changes when a programmer adds a clause to a pattern match, removes a clause from a pattern match, adds a constructor to a data type, or removes a constructor from a data type. Let us see why first-match semantics complicates reasoning about these kinds of changes.

If we want to understand the consequences of adding or removing a clause from a pattern match, then we have to consider all clauses occurring both above and below the clause we are changing. Having to reason about the entire context of the clause makes it much harder to spot bugs in code reviews, since it is not uncommon that pattern matching expressions can span multiple pages of code. Order-independent semantics guarantees that it doesn’t matter if we add, delete or modify a clause at the beginning, middle or end of a list of clauses.

The other kind of change that frequently occurs is that we add or remove a constructor from an existing data type. Whether we have to adjust existing pattern matches depends on how those have been written. Even if we enforce that clauses in a pattern matching expression must not overlap, we have multiple possibilities to write exhaustive pattern matches. Consider a data type “Group” which consists of administrators, registered users and guests. We want to guarantee that only administrators have write access, but we have two possibilities to write the function:

On the left side we have pattern matched exhaustively on the complement of Admin, whereas on the right side we have used a negation pattern. These two programs behave the same, but we can observe a difference when we add moderators as a fourth type of user. We have to revisit the function on the left, whereas the function on the right continues to compile.

Some programming languages have already started to add support for enforcing these kind of considerations. For example, Rust supports the #[non_exhaustive] attribute on type declarations²²2Cp. doc.rust-lang.org/stable/reference/attributes/type_system.html.. This attribute restricts pattern matches and ensures that they continue to compile after a new constructor has been added to the type; annotating the Group type with such an attribute would disallow the definition on the left. Dually, OCaml warns against writing “fragile pattern matches”. A fragile pattern can hide newly added constructors, which might have unintended consequences. The algebraic patterns presented in this paper provide the necessary tools to program in situations where the programmer wants to enforce either one of these dual restrictions. There is also some empirical evidence that programmers feel uneasy about using wildcard patterns in evolving codebases. For example, the authors of a recent study about the programming practices of functional programmers [21] write: “Participants felt similarly about the use of wildcards in pattern matching, which silently assign pre-existing behavior to new variants of an enumeration. P7 mentioned that, in their main codebase, wildcards are completely disallowed for this reason, even though they make programming more convenient.”

Our main motivation in this paper is to obtain a more declarative programming model for standard nominal data types and ordinary pattern matching. The compilation algorithm that we are presenting, however, also works for polymorphic variants [10]. Polymorphic variants are used in the programming language OCaml, for example, to handle open sets of possible error conditions without having to declare a data type which lists all possible errors. Our algorithm does not presuppose a data type declaration with a fixed set of constructors which is necessary to check for exhaustiveness; we do not discuss exhaustiveness of patterns in the main part of this paper, but outline the necessary modifications to check for it in the extended version [2]. We think that the ideas and the algebraic patterns that we present in this paper are also useful for some proposed solutions of the expression problem. In the compositional programming approach [25, 29, 28], for example, we can create pattern matches whose clauses are distributed among multiple different modules. In that scenario it is especially important to guarantee that the contributing clauses which come from different modules do not overlap in their left-hand side.

We will now present the formal rules which specify what happens when we match a pattern against a value; these rules can be found in the upper half of Figure 2. We use two mutually recursive judgments to formalize the semantics of matching: The judgment $p⊳v\rightsquigarrow \sigma$ expresses that the pattern $p$ successfully matches the value $v$ and also binds values to variables of the pattern; those mappings are recorded in the substitution $\sigma$. The judgment $p⋫v\rightsquigarrow \sigma$ expresses that the pattern $p$ does not match the value $v$, and also produces a substitution. That the judgment $p⋫v\rightsquigarrow \sigma$ also produces a substitution might be surprising: How can there be a substitution if the value does not match the pattern? We can think of these as “temporarily deactivated” substitutions which will become available again if we enclose the pattern in an additional negation. In fact, such substitutions are necessary if we want to guarantee that the pattern $p$ is semantically equivalent to $\neg \neg p$ in the case where $p$ contains variables, for example in Equation 5 below.

Using the rules for $p⊳v\rightsquigarrow \sigma$ and $p⋫v\rightsquigarrow \sigma$ we can already prove that they are, in a certain sense, sound and complete:

Since we are interested in algebraic reasoning, we have to say when we consider two patterns to be semantically equivalent. We will define semantic equivalence in Definition 6 using the two judgments introduced above. But first, we have to define when two substitutions (which we formalized as lists of mappings) are semantically equivalent:

We can now state the definition for semantic equivalence of patterns.

We have to include both judgment forms if we want semantic equivalence to be a congruence relation. To see why this is the case, suppose that we omit the second half of Definition 6. It would then follow that the two patterns $\mathrm{\#}$ and $\neg x$ are semantically equivalent since they match against the same set of values (i.e. no values at all). But if we apply a negation-pattern to both patterns, then we can easily show that the resulting patterns are no longer semantically equivalent: $⟦\neg \mathrm{\#}⟧\equiv ⟦\mathrm{\_}⟧\not\equiv ⟦x⟧\equiv ⟦\neg \neg x⟧$. But since Definition 6 requires both patterns to agree on the values they match and don’t match against, it actually defines a congruence relation on patterns:

We can use the definition of semantic equivalence to prove that the following algebraic laws hold for patterns:

In addition to these boolean laws we can also prove the following equivalences which involve constructor patterns:

There are still some equivalences that we expect to hold but which are missing from Theorem 8 and Theorem 9. These additional laws, like the distributive law for and- and or-patterns, are not universally valid and require additional restrictions on patterns. We will motivate and introduce these additional constraints in the next subsection.

The first restriction we impose on patterns is linearity. The linearity restriction is easy to state if the syntax of patterns does not include and-patterns, or-patterns and negation-patterns: A pattern is linear if every variable occurs at most once. To see why this restriction is necessary consider the nonlinear pattern $\mathrm{𝙲𝚘𝚗𝚜}(x,x)$, for which we can derive the following judgment:

The problem here is that multiple values are bound to the same variable, i.e. the result of the pattern match is not a proper substitution.

We have a more expressive language of algebraic patterns, and the simple definition of linearity described above is no longer sufficient. To see why this is the case, consider the pattern that is linear according to the simple definition, but which shows the following pathological behavior:

Equations 7 and 8 show that matching against this pattern can produce substitutions that do not have the same domain.

The two examples above tell us what the correct notion of linearity should guarantee: First, if a linear pattern matches against a value, then the resulting substitution should be a proper substitution which contains at most one mapping for a variable. Second, if we use a pattern in a clause we should be able to read off the variables that will be in the domain of the substitution of a successful match.

In order to ensure that these properties hold we have to use two mutually recursive judgments $p{\mathrm{𝐥𝐢𝐧}}^{+}$ and $p{\mathrm{𝐥𝐢𝐧}}^{-}$, whose rules are given in Figure 2. We use $p{\mathrm{𝐥𝐢𝐧}}^{\pm }$ for patterns which satisfy both $p{\mathrm{𝐥𝐢𝐧}}^{+}$ and $p{\mathrm{𝐥𝐢𝐧}}^{-}$. Theorems 10 and 11 show that linear patterns do have the properties described in the previous paragraph.

We will now motivate why the rules in Figure 2 have the specific form that they do. Theorem 10 tells us that we should think about the variables in ${\mathrm{FV}}^e(p)$ as the actual pattern variables which we can use in the right-hand side of a clause, and that we should think of the variables in ${\mathrm{FV}}^o(p)$ as the “temporarily deactivated” pattern variables “reactivated” by negation.

Let us first look at the restrictions on the variables in ${\mathrm{FV}}^e(p)$, since those are more intuitive. In the or-pattern $p_1\parallel p_2$ we require that ${\mathrm{FV}}^e(p_1)$ is equal to ${\mathrm{FV}}^e(p_2)$ since we do not know which of the two patterns will match, and we have to ensure that the same variables appear in the substitution. In the and-pattern we require that ${\mathrm{FV}}^e(p_1)$ is disjoint from ${\mathrm{FV}}^e(p_2)$ since we do not want the same variable to be mapped to two values in the substitution. The reasoning is very similar for constructor patterns $𝒞(p_1,\mathrm{\dots },p_i$) where we require all the ${\mathrm{FV}}^e(p_i)$ to be disjoint.

Next, let us look at the restrictions on ${\mathrm{FV}}^o(e)$, i.e. the variables which occur under an odd number of negations. The rules for and-patterns and or-patterns are motivated by duality. We have seen that the De Morgan rules are valid for patterns. We therefore want, for example, that if the pattern $\neg (p_1\parallel p_2)$ is linear, the pattern should be linear as well. For this to be true, the restrictions on ${\mathrm{FV}}^o(p)$ for or-patterns have to mirror the restrictions on ${\mathrm{FV}}^e(p)$ for and-patterns, and vice-versa. We still have to explain why we require for a constructor pattern $𝒞(p_1,\mathrm{\dots },p_n)$ that all ${\mathrm{FV}}^o(p_i)$ have to be the empty set. The reason for this restriction lies in the following semantic equivalence, which is motivated by its importance for rewriting patterns into a normal form (see Section 5.1) and which we will prove below.

The pattern on the right consists of several patterns that are joined by or-patterns. The rules for or-patterns require that each disjunct contains the same sets ${\mathrm{FV}}^e(-)$. But since the first pattern $\neg 𝒞(\mathrm{\_},\mathrm{\dots },\mathrm{\_})$ doesn’t contain any variables, the other disjuncts must not contain any variables under an even number of negations. And since the subpatterns $p_i$ occur under a negation, we can deduce that the patterns $p_i$ must not contain any variables under an odd number of negations.

Using linearity we can now prove the missing equivalences which were not included in Theorems 8 and 9.

Theorem 8 and Theorem 12 taken together show that patterns form a boolean algebra, with the caveat that the conjunction or disjunction of two linear patterns does not necessarily result in a linear pattern. We can also prove some additional equivalences involving constructor patterns.

The equivalences of Theorem 13 are essential for proving the correctness of the normalization algorithm specified in Section 5.

We also have to introduce a notion of deterministic patterns. To see why this is necessary, consider the pathological pattern $\mathrm{𝙿𝚊𝚒𝚛}(x,\mathrm{\_})\parallel \mathrm{𝙿𝚊𝚒𝚛}(\mathrm{\_},x)$. This pattern is linear, but when we match against the value $\mathrm{𝙿𝚊𝚒𝚛}(2,4)$ we can either bind the value $2$ or the value $4$ to the variable $x$. Deterministic patterns guarantee that when there are multiple derivations which show that a pattern matches against a value, then these alternatives must yield equivalent substitutions³³3Most languages which implement or-patterns do not check whether patterns are deterministic and instead evaluate or-patterns left-to-right, but this invalidates algebraic laws such as the commutativity of or-patterns. If we need such left-biased or-patterns $p{\parallel }^{\leftarrow }q$ then we can easily define them as . .

To define deterministic patterns we first have to introduce overlapping and disjoint patterns. In the extended version [2] we give a procedure for deciding whether two patterns in a certain normalized form – which we will introduce in Section 5 – overlap.

We write $p\mathrm{𝐝𝐞𝐭}$ for patterns which satisfy the determinism restriction specified in Figure 2. Note that there are two rules for or-patterns: The rule D-Or₁ says that an or-pattern is deterministic if the subpatterns are disjoint, whereas the rule D-Or₂ allows arbitrary deterministic subpatterns as long as they do not contain free variables. As for the linearity restriction, these two rules for or-patterns give rise to corresponding rules for and-patterns via De Morgan duality: Given that the pattern $\neg (p1\parallel p2)$ is deterministic, we want the semantically equivalent pattern to be deterministic as well.

This property is also necessary to show that the evaluation of terms is deterministic, since we use the relation $p⊳v\rightsquigarrow \sigma$ when we define the evaluation of pattern matches in the next subsection.

Expressions $e$ consist of variables $x$, the application of a constructor to arguments $𝒞(e_1,\mathrm{\dots },e_n)$ and case expressions. Every case expression consists of a scrutinee, a list of normal clauses $c$ which all have the form $p\Rightarrow e$, and a default clause $\mathrm{𝐝𝐞𝐟𝐚𝐮𝐥𝐭}\Rightarrow e$.

Every case expression contains exactly one default clause, but a realistic language would also allow to omit the default clause if all other clauses are exhaustive. As we already mentioned, $\mathrm{𝐝𝐞𝐟𝐚𝐮𝐥𝐭}$ does not belong to the syntax of patterns, but to the syntax of case expressions. In particular, the meaning of a default clause is not equal to the meaning of a clause $\mathrm{\_}\Rightarrow e_d$ which uses a wildcard pattern, but equal to a clause , where the $p_i$ are all the patterns from the other clauses of the case expression. For this reason it is not possible to define the meaning of a default clause in isolation, unlike for normal clauses, and a default clause also does not immediately give rise to a valid equation for term rewriting.

We formalize a call-by-value semantics in which the only values $v$ are constructors applied to other values. We use evaluation contexts $E$ and a congruence rule E-Cong to specify evaluation within a subterm, following standard practice [9].

We write $e{\to }^r{e}^{\prime }$ for the single-step reduction of the expression $e$ to $e^{\prime }$ which does not use the congruence rule, and $e\to e^{\prime }$ for the single step reduction within an evaluation context. The evaluation of case expressions is governed by the two rules E-Match and E-Default. The rule E-Match allows to reduce a case expression using any of the normal clauses that match the scrutinee; in particular, it is not necessary to try the clauses in the order in which they occur. On the right-hand side of that rule we write $e\sigma$ for the result of applying the substitution $\sigma$ to the expression $e$. The rule E-Default allows to reduce a case expression to the expression of the default clause if none of the other clauses match against the scrutinee.

Single-step evaluation: $e\to e$

Nothing in these rules guarantees that evaluation is deterministic. For example, we can write a case expression with overlapping patterns. If we want evaluation to be deterministic, then we have to check that expressions are wellformed, written as $e\mathrm{✓}$. For this we have to check that all patterns which occur in case expressions are deterministic, positively linear, and that no two clauses in a case expression have overlapping patterns.

Wellformed expressions: $e\mathrm{✓}$

The evaluation of wellformed expressions is deterministic. Furthermore, to check whether an expression is wellformed does not depend on any type information.

Multi-step evaluation ${\to }^{\ast }$ is defined as the reflexive-transitive closure of single-step evaluation and allows us to define when two closed expressions are semantically equivalent:

This theorem makes formal what we call pure no-overlap semantics for pattern matching. The next theorem guarantees that we can use algebraic principles when reasoning about patterns in clauses.

In this section, we are going to introduce types, typing contexts and (pattern) typing rules. In order to illustrate the typing rules we include three simple data types: the boolean type $𝔹$ with constructors $\mathrm{𝚃𝚛𝚞𝚎}$ and $\mathrm{𝙵𝚊𝚕𝚜𝚎}$, the type of pairs $\tau \otimes \tau$ with the constructor $\mathrm{𝙿𝚊𝚒𝚛}$, and the type of binary sums $\tau \oplus \tau$ with constructors ${\iota }_1$ and ${\iota }_2$.

We use the judgment $\mathrm{\Gamma };\mathrm{\Delta }\Rightarrow p:\tau$ to express that the pattern $p$ matches against a value of type $\tau$ and binds variables whose types are recorded in the context $\mathrm{\Gamma }$ on a successful match, and in context $\mathrm{\Delta }$ in the case of a non-successful match. In other words, the typing context $\mathrm{\Gamma }$ is used for typing the pattern variables that occur under an even number of negations, and the typing context $\mathrm{\Delta }$ is used for typing the variables under an odd number of negations. We write ${\mathrm{\Gamma }}_1++{\mathrm{\Gamma }}_2$ for the naive concatenation of two typing contexts.

Pattern typing: $\mathrm{\Gamma };\mathrm{\Delta }\Rightarrow p:\tau$

These pattern typing rules do not make sense on their own, but only in conjunction with the rules for linearity. For example, the typing rules allow to derive the typing judgment $x:{\tau }_1,x:{\tau }_2;\cdot \Rightarrow \mathrm{𝙿𝚊𝚒𝚛}(x,x):{\tau }_1\otimes {\tau }_2$, but the linearity rules disallow this pattern⁴⁴4 An implementation might choose to check linearity and typing of patterns simultaneously, but we prefer to present them separately to illustrate that we can also use algebraic patterns in the untyped setting. . Lastly, we present the rules for typing expressions:

Expression typing: $\mathrm{\Gamma }⊢e:\tau$

In the rule T-Match we use the pattern typing rule for the pattern in each clause, and add the resulting typing context ${\mathrm{\Gamma }}_i$ which contains the types of all pattern variables under an even number of negations to the outer typing context $\mathrm{\Gamma }$ in the respective clause.

Consider the pattern $\neg \mathrm{𝙿𝚊𝚒𝚛}(\mathrm{𝚃𝚛𝚞𝚎},\mathrm{𝙵𝚊𝚕𝚜𝚎})$ which matches anything except a tuple consisting of the boolean values $\mathrm{𝚃𝚛𝚞𝚎}$ and $\mathrm{𝙵𝚊𝚕𝚜𝚎}$. Another way to express the behavior of this pattern is to say that it matches anything which isn’t a tuple, or it matches a tuple if either the left element isn’t the value $\mathrm{𝚃𝚛𝚞𝚎}$ or the right element isn’t the value $\mathrm{𝙵𝚊𝚕𝚜𝚎}$. We can therefore also write the pattern as $\neg \mathrm{𝙿𝚊𝚒𝚛}(\mathrm{\_},\mathrm{\_})\parallel \mathrm{𝙿𝚊𝚒𝚛}(\neg \mathrm{𝚃𝚛𝚞𝚎},\mathrm{\_})\parallel \mathrm{𝙿𝚊𝚒𝚛}(\mathrm{\_},\neg \mathrm{𝙵𝚊𝚕𝚜𝚎})$. We can generalize this observation and use it to push all negation-patterns inside, by repeatedly rewriting the pattern using the last equation of Theorem 13. After we have normalized patterns in this way, negation-patterns only occur applied to variables or to constructors where all subpatterns of the constructor are wildcard patterns. We abbreviate these negated constructor patterns $\neg {𝒞}^n(\mathrm{\_},\mathrm{\dots },\mathrm{\_})$ as $\neg {𝒞}^n$.

The normalization procedure $\mathrm{𝚗𝚗𝚏}(-)$ is split into the two functions ${\mathrm{𝚗𝚗𝚏}}^{-}(-)$ and ${\mathrm{𝚗𝚗𝚏}}^{+}(-)$ which track if we are currently normalizing a negated or a non-negated pattern. At the top-level, the function $\mathrm{𝚗𝚗𝚏}(-)$ therefore just invokes ${\mathrm{𝚗𝚗𝚏}}^{+}(-)$.

We treat the negation normal forms $N$ as a subset of patterns $p$, and hence all functions and properties of patterns can also be applied to normal forms. If we translate a pattern into negation normal form then the pattern is still wellformed, can be typed using the same context and type, and has the same semantics as before. This is witnessed by the following lemma.

The next step is to bring the negation normal form into a disjunctive normal form. Patterns in disjunctive normal form consist of an outer disjunction of so-called “elementary conjuncts” which do not contain or-patterns. The syntax of the disjunctive normal forms $D$ and elementary conjuncts $K$ is given below. We can normalize a pattern in negation normal form to the disjunctive normal form by the function $\mathrm{𝚍𝚗𝚏}(-)$ which takes a pattern in negation normal form and returns a set of elementary conjuncts. At the top-level we have to wrap the result in a $\parallel \{\mathrm{\dots }\}$ node.

We can embed the disjunctive normal form $\parallel \{K_1,\mathrm{\dots },K_n\}$ into patterns as $K_1\parallel \mathrm{\dots }\parallel K_n$. This set of conjuncts is by design never empty ($n>0$), however, if we do admit this case ($n=0$) it translates to the absurd-pattern $\mathrm{\#}$ and is treated as such in any use case (see Section 6).

As a last step, we further simplify the elementary conjuncts of Section 5.2. We write $\overline{D}$ and $\overline{K}$ for these normalized disjunctive normal forms and normalized elementary conjuncts:

These normalized conjuncts follow from the observation that there are essentially only three different kinds of conjuncts: positive, negative and unsatisfiable. Each of these three conjuncts can bind a set of variables $\{x_1,\mathrm{\dots },x_n\}$. A positive conjunct matches against any value headed by the constructor $𝒞$, and binds that value against all the variables in the set. A negative conjunct matches against any value which is headed by a constructor which is not in the list $\{{𝒞}_1,\mathrm{\dots },{𝒞}_m\}$. The negative conjunct can be used to represent a single pattern variable $x$, and similarly can be used to represent a wildcard pattern. An unsatisfiable conjunct never matches against a value.

Computing these normalized conjuncts consists in collecting all the variables, as well as all negated and non-negated head constructors of an elementary conjunct. Intuitively, the head constructors are constructors that occur in a pattern without being nested in a subpattern of another constructor. An elementary conjunct is unsatisfiable if two different non-negated constructors appear in the conjunct, or if a head constructor appears both negated and non-negated. An elementary conjunct can be simplified to a negative conjunct if only negated head constructors appear in the original conjunct. Lastly, an elementary conjunct can be simplified to a positive conjunct if neither of the two cases above apply. We write $\mathrm{𝚗𝚘𝚛𝚖}(-)$ for the function which computes these normalized conjuncts; the formal definition of this function is given in the appendix of the extended version of this paper [2]. We also remove negated variables in this step and treat them like absurd patterns; this is, strictly speaking, not semantics preserving, but negated variables cannot be used in the right-hand side of a clause anyway, so this has no effect on the compilation of programs.

Like in Section 5.2, we treat the normal forms $\overline{D}$ and $\overline{K}$ as subsets of patterns $p$. We use patterns in normalized disjunctive normal form in the next section where we define a pattern matching compilation algorithm for nested patterns.

The algorithm operates on a generalization of the case expression $\mathrm{𝐜𝐚𝐬𝐞}v\mathrm{𝐨𝐟}\{p_1\Rightarrow e_1,\mathrm{\dots },p_n\Rightarrow e_n;\mathrm{𝐝𝐞𝐟𝐚𝐮𝐥𝐭}\Rightarrow e\}$ that we introduced in Section 4.1. Instead of only one scrutinee $v$ and one pattern $p$ in each clause we now allow a vector $v_1,\mathrm{\dots },v_n$ of scrutinees and a matrix of clauses with patterns in nDNF (see Section 5.3).

In such multi-column case expressions, the $i$-th pattern column tests the $i$-th scrutinee $v_i$. The main idea of the algorithm is that we take such a multi-column case expression as input and examine all scrutinees – and subscrutinees – one by one, producing a nesting of single-column case expressions with simple patterns as output. These simple patterns consist only of constructors applied to variables. We start the compilation by embedding an ordinary case expression into this generalized form on which we call the function compile. This function can take one of three steps. It either terminates with a Default or Simple step, or it examines one of the scrutinees in a Branch step.

Default

If $\mathrm{𝐝𝐞𝐟𝐚𝐮𝐥𝐭}\Rightarrow e_d$ is the only clause then we terminate with the expression $e_d$.

Simple

If the first row consists only of variable patterns of the form then compilation terminates with the right-hand side of that clause together with appropriate substitutions. This rule also applies if $n=0$.

Branch

If neither of the above steps apply we pick a column $i$ (with $1\le i\le n$) and examine its scrutinee $v_i$ in a single-column case against simple constructor patterns.

All the complexity of the algorithm lies within the Branch step, so we will discuss its details in the next subsection.

The first step is to choose on which index $i$ we want to perform the case split. This choice does not affect the correctness of the algorithm; selecting a column is a therefore a matter of optimization which other authors [26, 23] have discussed in detail. We only enforce that the selected pattern column must contain outermost constructors. Such a column must necessarily exist if neither the Default nor the Simple step apply.

Next, we have to gather the constructors against which we can test the scrutinee $v_i$. We collect these so-called head constructors into a set $\mathscr{H}({\overline{D}}_i)$ defined below.

Once we have found these head constructors $\{{𝒞}^{n_1},\mathrm{\dots },{𝒞}^{n_z}\}$ we generate fresh pattern variables $x_1^k$ to $x_{n_k}^k$ for each constructor ${𝒞}^{n_k}$ and a simple pattern match. For each clause we have gained information about the scrutinee $v_i$: Within the right-hand side of a constructor clause, we know that our scrutinee must have conformed to the shape of our constructor. Likewise, if we arrive at the right-hand side of the default clause, we know that our scrutinee must have been different to all the constructors $\{{𝒞}^{n_1},\mathrm{\dots },{𝒞}^{n_z}\}$ before. We use this knowledge by computing clause-specific subproblems of our initial Input and we do so via the function $𝒮$ for constructor clauses and function $𝒟$ for the default clause.