6Defining Matchers

This chapter explains how users can define their own matchers.

6.1`inductive pattern` Declaration

When defining a matcher, the pattern constructors that the matcher handles must be declared in advance using an inductive pattern declaration.

An inductive pattern declaration is a syntax for declaring the types of pattern constructors independently from the definitions of data constructors and matchers. For example, the pattern constructors for the list type [a] are declared as follows.

inductive pattern [a] :=
  | []
  | (::) a [a]
  | (++) [a] [a]

This declaration states that the pattern constructors [], ::, and ++ are all pattern constructors targeting the list type [a]. The types following each pattern constructor represent the types of that pattern constructor's arguments—that is, the types of the values passed as next targets upon successful pattern matching.

An important feature of inductive pattern declarations is that a pattern constructor such as :: is shared across multiple matchers, including the list matcher, the multiset matcher, and the set matcher. Each matcher implements a different decomposition method for ::, but the type of the pattern constructor is managed centrally through the inductive pattern declaration.

matchAll [1, 2, 3] as list integer with
  | $x :: $xs -> (x, xs)
-- [(1,[2,3])]

matchAll [1, 2, 3] as multiset integer with
  | $x :: $xs -> (x, xs)
-- [(1,[2,3]),(2,[1,3]),(3,[1,2])]

Even with the same pattern $x :: $xs, the meaning (decomposition method) changes depending on which matcher is used.

The relationship between inductive pattern declarations and matcher definitions is analogous to the relationship between type classes and instance definitions. Just as a type class declaration declares the types of methods and an instance definition provides their concrete implementations, an inductive pattern declaration declares the types of pattern constructors and a matcher definition provides the concrete decomposition methods for those pattern constructors.

Type classes	Pattern matching
Type class declaration	Inductive pattern declaration
Instance definition	Matcher definition
Method name	Pattern constructor name
Method type	Pattern constructor type
Instance dispatch (static)	Matcher dispatch (dynamic)

However, unlike type class instance selection, which is statically determined at compile time, matcher selection is explicitly specified by the user at runtime in match and matchAll expressions (dynamic selection).

6.2Basics of Matcher Definitions

This section explains the basics of matcher definitions by examining the matcher definition for unordered pairs (pairs that ignore the order of elements), one of the simplest non-free data types.

First, let us confirm the behavior of the unorderedIntegerPair matcher for unordered pairs of integers. Using the pair pattern with unorderedIntegerPair, both orderings of the elements are matched as follows.

matchAll (1, 2) as unorderedIntegerPair with
| pair $x $y -> (x, y)
-- [(1,2),(2,1)]

Thanks to this, pattern matching succeeds even when the first argument of pair is the second element of the target.

matchAll (1, 2) as unorderedIntegerPair with
| pair #2 $y -> y
-- [1]

When the pattern is a pattern variable, the target is bound as is.

matchAll (1, 2) as unorderedIntegerPair with
| $p -> p
-- [(1,2)]

The unorderedIntegerPair matcher that behaves as described above can be defined as follows. First, the pair pattern constructor must be declared with an inductive pattern declaration.

inductive pattern (Integer, Integer) :=
  | pair Integer Integer

This declaration states that pair is a pattern constructor targeting the integer pair type (Integer, Integer) and takes two arguments of type Integer. Next, the unorderedIntegerPair matcher is defined as follows, with a type annotation indicating that it is a matcher for integer pairs.

def unorderedIntegerPair : Matcher (Integer, Integer) := matcher
  | pair $ $ as (integer, integer) with
    | ($x, $y) -> [(x, y), (y, x)]
  | $ as something with
    | $tgt -> [tgt]

matcher is a built-in syntax for creating matchers.

matcher
| `primitive pattern-pattern` as `next matcher expression` with
  | `primitive data pattern` -> `body`
  ...
...

A matcher expression takes multiple matcher clauses. A matcher clause consists of a primitive pattern-pattern, a next matcher expression, and multiple primitive match clauses. A primitive match clause consists of a primitive data pattern and a body.

Let us examine the first matcher clause of unorderedIntegerPair (lines 2--3). First, the primitive pattern-pattern of this matcher clause is pair $ $. A primitive pattern-pattern is a pattern on patterns. This primitive pattern-pattern matches the pair pattern, and this matcher clause defines how pattern matching is performed for the pair pattern. A pattern constructor that appears in a primitive pattern-pattern, such as pair, is called a primitive pattern-pattern constructor. The $ appearing as arguments of the pair pattern is called a pattern hole, a component of primitive pattern-patterns that matches any pattern. A pattern that matches a pattern hole is called a next pattern. Pattern matching of primitive pattern-patterns is performed in essentially the same way as pattern matching on algebraic data types in typical functional programming languages. Next, the next matcher expression of this matcher clause is (integer, integer). This expresses that the two patterns bound to the pattern holes above (the arguments of the pair pattern) will be recursively pattern-matched using the integer matcher. This matcher clause takes one primitive match clause (line 3). The primitive data pattern is matched against the target. Pattern matching of primitive data patterns is also performed in essentially the same way as pattern matching on algebraic data types in typical functional programming languages. The body of a primitive match clause returns the decomposition results of the target. (x, y) and (y, x) are called next targets and are recursively pattern-matched using the next patterns and next matchers.

The primitive pattern-pattern of the second matcher clause (lines 4--5) is a pattern hole. Since a pattern hole matches any pattern, all patterns not matched by the first matcher clause are handled by the second matcher clause. The only patterns for unorderedIntegerPair that do not match the first matcher clause are wildcards and pattern variables, so this matcher clause handles these patterns. This matcher clause simply changes the matcher to something without changing the pattern or target. The pattern and target are then pattern-matched using something. something is the only built-in matcher and handles the following three types of patterns.

Wildcard: Always succeeds in pattern matching without producing any bindings.
Pattern variable $x: Succeeds in pattern matching and binds the target value to x.
Value pattern #e: Evaluates the expression e and compares the result with the target value using built-in structural equality (equality comparison based on the structure of data constructors). If they are equal, the pattern match succeeds.

The handling of value patterns directly by something is a design change accompanying the introduction of static typing (see Section 6.3 below for details).

The following unorderedPair can be defined as a matcher for unordered pairs that takes a matcher for the data type of the pair's elements as an argument.

matchAll (1, 2) as unorderedPair integer with
| pair $x $y -> (x, y)
-- [(1,2),(2,1)]

To do this, first change the inductive pattern declaration to a generic form using type parameters.

inductive pattern {a} (a, a) :=
  | pair a a

Then, define unorderedPair as a function that takes a matcher as an argument and returns a matcher. The next matcher expression of the matcher clause for the pair pattern uses m, the argument of unorderedPair. The type annotation indicates that it takes a type parameter {a} and a matcher argument (m: Matcher a), and returns a matcher for the pair type (a, a).

def unorderedPair {a} (m: Matcher a) : Matcher (a, a) := matcher
  | pair $ $ as (m, m) with
    | ($x, $y) -> [(x, y), (y, x)]
  | $ as something with
    | $tgt -> [tgt]

6.3Definition of the `eq` Matcher

The eq matcher can also be defined by the user using a matcher expression. The eq matcher handles only value patterns, wildcards, and pattern variables, so it has no special pattern constructors. Therefore, no inductive pattern declaration is needed for the eq matcher itself. The type annotation indicates that it is a matcher for a type parameter a with the type constraint {Eq a}.

def eq {Eq a} : Matcher a := matcher
  | #$val as () with
    | $tgt -> if val == tgt then [()] else []
  | $ as something with
    | $tgt -> [tgt]

The first matcher clause of the eq matcher (lines 2--3) is a matcher clause for value patterns. #$val is a primitive pattern-pattern that matches value patterns. Such a primitive pattern-pattern is called a primitive value pattern. The variable val is bound to the content of the value pattern. Since the primitive pattern-pattern of this matcher clause does not contain any pattern holes, the next matcher expression is the empty tuple. The primitive match clause checks whether the content of the value pattern and the target value are equal.

Difference between `something` and `eq`.

something handles value patterns using built-in structural equality, while eq compares using the user-defined == operator, which is a method of the Eq type class. The distinction between these two is deeply related to the design of matchers that take matchers as arguments (matcher-parameterized matchers).

For example, when processing a value pattern in a matcher like multiset that takes an argument matcher m, the question arises as to which matcher should handle the base case of recursive comparison. If something could not handle value patterns, the only option would be to delegate to the eq matcher, and since eq requires the Eq type class constraint, the type of multiset would become multiset : {Eq a} => Matcher a -> Matcher [a], requiring the Eq constraint. However, since many uses of multiset do not use value patterns, this constraint would be overly restrictive.

To solve this problem, built-in structural equality-based value pattern handling was incorporated into something. This allows matcher-parameterized matchers to use something as the base case without imposing type class constraints, giving multiset : Matcher a -> Matcher [a], a type without constraints. On the other hand, when user-defined equality comparison (==) is desired, one can explicitly specify the eq matcher.

Primitive pattern-patterns consist of the four components we have seen so far: pattern holes, applications of primitive pattern-pattern constructors, primitive value patterns, and primitive wildcards.

`primitive pattern-pattern` ::= $ | c `primitive pattern-pattern`* | #$`ID` | _

Usage examples of primitive wildcards are presented in Section 6.6.

Primitive data patterns consist of wildcards, pattern variables, and applications of primitive data pattern constructors.

`primitive data pattern` ::= _ | $`ID` | C `primitive data pattern`*

6.4Definition of the `multiset` Matcher

This section explains the definition of the multiset matcher. The multiset matcher handles the pattern constructors ([], ::, ++) declared in the inductive pattern declaration for the list type [a] shown in Section 6.1. The type annotation indicates that it takes a type parameter {a} and a matcher argument (m: Matcher a), and returns a matcher for the list type [a].

def multiset {a} (m: Matcher a) : Matcher [a] := matcher
  | [] as () with
    | $tgt -> match tgt as (mutiset m) with
                | [] -> [()]
                | _ -> []
  | $ :: $ as (m, multiset m) with
    | $tgt -> matchAll tgt as list m with
                | $hs ++ $x :: $ts -> (x, hs ++ ts)
  | #$val as () with
    | $tgt -> match (val, tgt) as (list m, multiset m) with
                | ([], []) -> [()]
                | ($x :: $xs, #x :: #xs) -> [()]
                | (_, _) -> []
  | $ as something with
    | $tgt -> [tgt]

The first and fourth matcher clauses are nearly self-explanatory, so let us examine the second and third matcher clauses.

Let us look at the second matcher clause (lines 6--8). The primitive pattern-pattern is $ :: $ , and the next matcher expression is (a, multiset a). Here, a is the argument matcher of multiset. The next targets are defined using a matchAll expression. When the target is [1,2,3], this matchAll expression returns [(1,[2,3]),(2,[1,3]),(3,[1,2])]. Each next target contained in this list is recursively pattern-matched using the next patterns and next matchers. For example, the next targets 1 and [2,3] are pattern-matched with the first and second arguments of the cons pattern using the next matchers a and multiset a.

Let us look at the third matcher clause. The primitive pattern-pattern of this matcher clause is the primitive value pattern #$val. This matcher clause handles value patterns. This matcher clause compares whether the content of the value pattern (val) and the target (tgt) are equal. The first and third match clauses of this match expression are self-explanatory, so we omit their explanation. The pattern of the second match clause extracts the first element of val from tgt. It then recursively pattern-matches the collection obtained by removing one identical element from both val and tgt, using the patterns $xs and #xs. Although this matcher clause is recursively called during the pattern matching of #xs, since the length of the collection decreases by one each time, it eventually reaches either the first or third match clause.

6.5Definition of the `sortedList` Matcher

The program that enumerates pairs of primes of the form $$(p,p+6)$$ using doubly nested join-cons patterns takes increasingly longer to enumerate later pairs of primes. The reason is that the doubly nested join-cons pattern examines all combinations of primes. For example, this pattern examines all prime pairs such as $$(3,5)$$ , $$(3,7)$$ , $$(3,11)$$ , $$(3,13)$$ , $$(3, 17)$$ , $$(3,19)$$ . However, starting from $$(3,11)$$ —the first prime pair whose difference exceeds $$6$$ —there is no need to check whether they are of the form $$(p,p+6)$$ .

take 10 (matchAll primes as sortedList integer with
         | _ ++ $p :: (_ ++  #(p + 6) :: _) -> (p, p + 6))
-- [(5,11),(7,13),(11,17),(13,19),(17,23),(23,29),(31,37),(37,43),(41,47),(47,53)]

By using a matcher specialized for sorted lists, this unnecessary search can be avoided. By adding a matcher clause with $ ++ #$px : $ as the primitive pattern-pattern to the standard list matcher, a matcher specialized for sorted lists can be created. This matcher clause reduces the computational complexity of the doubly nested join-cons pattern that matches prime pairs of the form $$(p,p+6)$$ from $$O(n^2)$$ to $$O(n)$$ . The type annotation indicates that it takes a type parameter a with the type constraint {Ord a} and a matcher argument (m: Matcher a), and returns a matcher for the sorted list type [a].

def sortedList {Ord a} (m: Matcher a) : Matcher [a] := matcher
  | $ ++ #$px :: $ as (sortedList m, sortedList m) with
    | \$tgt -> matchAll tgt as list m with
               | loop $i (1, $n)
                   ((?(\x -> x < px) & $h_i) :: ...)
                   (#px :: $ts)
                 -> (map (\i -> h_i) [1..n], ts)
  ...

This optimization, which defines a pattern-matching algorithm directly for nested patterns, is called pattern fusion.

6.6Optimization with Primitive Wildcards

When a pattern contains wildcards, pattern matching can be sped up by omitting the computation of targets that match wildcards. In Egison, this optimization can be performed by using primitive wildcards in primitive pattern-patterns. This section presents such an optimization for the multiset matcher introduced in Section 6.4. This kind of optimization is called wildcard optimization.

The target of the optimization presented in this section is the case where the second argument of the cons pattern is a wildcard. In this case, there is no need to compute the remaining collection after removing one element from the target collection. By using primitive wildcards, we can instruct the multiset matcher to skip this computation.

matchAll [1, 2, 3, 4, 5] as multiset eq with
| $x :: _ -> x
-- [1, 2, 3, 4, 5]

This optimization can be achieved by adding the matcher clause on lines 2--3 below to the definition of the multiset matcher from Section 6.4. A primitive wildcard is used in the primitive pattern-pattern of this matcher clause. Since the pattern hole is only in the first argument of the cons pattern, the next matcher is just m, and since the next target is each element of tgt, tgt is returned as is.

def multiset {a} (m: Matcher a) : Matcher [a] := matcher
  | $ :: _ as m with
    | $tgt -> tgt
  | $ :: $ as (m, multiset m) with
    | $tgt -> matchAll tgt as list m with
              | $hs ++ $x :: $ts -> (x, hs ++ ts)
  ...

The sortedList matcher from Section 6.5 can be similarly optimized. The matcher clause on lines 2--7 below serves to skip the computation of the first argument of the join pattern.

def sortedList {Ord a} (m: Matcher a) : Matcher [a] := matcher
  | _ ++ #$px :: $ as sortedList m
    | \tgt -> matchAll tgt as list m with
              | loop $i (1, _)
                  (?(\x -> x < px) :: ...)
                  (#px :: $ts)
                -> ts
  | $ ++ #$px :: $ as (sortedList m, sortedList m)
    | \tgt -> matchAll tgt as list m with
              | loop $i (1, $n)
                  ((?(\x -> x < px) & $h_i) :: ...)
                  (#px :: $ts)
                -> (map (\i -> h_i) [1..n], ts)
  ...

6.7The `assocMultiset` Matcher

Egison provides assocMultiset as a matcher for multisets. This section introduces its usage and definition.

A multiset can be represented as an association list of elements and their multiplicities. The assocMultiset matcher is a matcher for multisets represented as such association lists. For example, the following program performs pattern matching on a multiset containing $$4$$ copies of $$1$$ , $$3$$ copies of $$2$$ , and $$1$$ copy of $$3$$ . A pattern that extracts elements appearing $$3$$ or more times in the target multiset is expressed.

matchAll [(1, 4), (2, 3), (3, 1)] as assocMultiset eq with
  | $x ^ #3 :: $rs -> (x, rs)
-- [(1, [(1, 1), (2, 3), (3, 2)]), (2, [(1, 4), (3, 2)])]

6.8Types of Matchers and Patterns

The matcher definitions so far carried type annotations such as Matcher (Integer, Integer). From this section on, we explain how pattern matching is checked by the type system.

In Egison's type system, matchers and patterns each have types. Matcher a is the type of matchers whose targets have type a, and Pattern a is the type of patterns that match values of type a. Matchers are first-class values, so functions such as multiset that take a matcher and return a matcher also have types. For example, the basic collection matchers have the following types.

something : Matcher a
eq        : {Eq a} => Matcher a
list      : MatcherSlot a a -> Matcher [a]
multiset  : MatcherSlot a a -> Matcher [a]
set       : MatcherSlot a a -> Matcher [a]

Argument-matcher positions use the slot type MatcherSlot a b, not Matcher. A slot type takes two types. The first component a is the type of the decomposition (structure) demanded by the pattern used at that position, and the second component b is the type of the target (the value being decomposed) there. When the two coincide, as at the element position of list and multiset, one may read it as “takes roughly a Matcher a”. The reason a slot type carries the decomposition type and the target type separately is to check, per use site, whether the matcher supplied there can actually decompose the pattern at that position. We return to this check in Section 6.10.

One design point hides in this list of types: the types of list and multiset carry no Eq constraint. Value patterns (such as #5) are handled at the level of something by structural equality, so the collection matchers themselves demand no equality on the elements. Thanks to this, matchers such as multiset can be used as-is even at types without a defined equality (symbolic mathematical expressions, abstract syntax trees, and so on). Using the eq matcher explicitly, as in intersect of Section 2.10 of Chapter 2, is for matching with the custom equality of an Eq type-class instance.

6.9Type Checking of Patterns

Patterns are typed independently of the matcher they are used with (matcher polymorphism). For example, $x :: $xs has type Pattern [a], which is exactly why the same pattern can be used with both list integer and multiset integer.

Type checking of value patterns involves the order of bindings. A pattern is checked from left to right with a growing set of bindings, and the expression e of a value pattern #e may refer to the pattern variables bound so far.

matchAll [1, 2, 3, 1] as multiset integer with
  | $x :: #x :: _ -> x
-- [1, 1]

This non-linear pattern expresses “some element x together with another occurrence of the same value”, and #x is type-checked under the binding of the preceding $x (of type Integer).

The type checker detects statically the mistakes that a dynamic implementation would answer only with a silent match failure. First, type errors inside a value pattern's expression are reported directly.

matchAll [1, 2, 3] as multiset integer with
  | $x :: #(x ++ [1]) :: _ -> x
-- Type error: (++) expects [Integer] but x is Integer

Second, a value pattern placed at the wrong position is detected.

matchAll [1, 2, 3] as multiset integer with
  | $x :: #x -> x
-- Type error: the second argument of :: requires
--   Pattern [Integer], but #x has type Pattern Integer

The programmer's intent was “x appears again in the rest”, but the second argument of :: is the position matching the whole remaining list; the correct pattern is $x :: #x :: _. A dynamic implementation would simply fail to match, reporting nothing. Finally, referring to a variable to the left of its binding is detected as an unbound-variable warning (and as a type error in strict mode).

matchAll [1, 2, 3] as multiset integer with
  | #x :: $x :: _ -> x
-- Warning: unbound variable x
--   (#x refers to x left of its binding $x)

6.10Type Checking of `match` Expressions

In match and matchAll expressions, the types of the target, the matcher, the patterns, and the bodies must all agree. If the target has type a, the matcher must have type Matcher a, every match clause's pattern must have type Pattern a, and the bodies of all match clauses must share one type.

For example, combining a collection pattern constructor with an integer matcher is a type error.

matchAll 5 as integer with
  | $x :: _ -> x
-- Type error: :: targets collections [a], but the
--   target and the matcher are for Integer

Body type mismatches are detected as well. In the twin example of Section 2.9 of Chapter 2, writing the body as [n, ns] is a type error because the list would mix Integer and [Integer]; a tuple (n, ns) is used instead.

In addition, the checker verifies that the matcher can provide the decomposition the pattern demands (the admissibility check). A pattern using only variable and value patterns demands no decomposition, so it combines with something at any type; a pattern using a constructor such as :: needs a matcher that can decompose it. Since something only matches any value as a whole and offers no means of decomposition, combining it with a cons pattern is a type error.

matchAll [1, 2, 3] as something with
  | $x :: $xs -> (x, xs)
-- Type error: something (Matcher a) does not fit
--   MatcherSlot [_] [Integer]
--   (something offers no way to decompose a list)

This is why matcher-receiving positions are typed with a slot type rather than Matcher. Here the cons pattern demands [_] (list decomposition) in the slot's decomposition component, which something cannot provide. A naive type system that treats something as Matcher [Integer] would accept this expression and then get stuck at runtime, where something cannot decompose a cons. Egison's type system checks decomposition admissibility per use site, so it rejects the error statically. This check is computed from the structure of the pattern alone, so wrong combinations are rejected statically, without running the matcher.

6.11Consistency of Matcher Definitions

Matcher definitions themselves are also type-checked. For each matcher clause, besides the type agreement of the primitive pattern pattern, the next-matcher expression, and the primitive data patterns, the exhaustiveness of the data-pattern arms is required. Once a clause's primitive pattern pattern matches the pattern, the target is matched against that clause's arms alone, and missing all of them is a runtime error. A matcher definition whose arm set is not exhaustive is therefore rejected as a type error.

def bad {a} (m : MatcherSlot a a) : Matcher [a] :=
  matcher
    | $ :: $ as (m, bad m) with
      | $x :: $xs -> [(x, xs)]    -- missing final | _ -> []
    | $ as something with
      | $tgt -> [tgt]
-- Type error: the data-pattern arms of matcher
--   clause :: $ $ are non-exhaustive

If the cons clause has only the arm $x :: $xs, an empty-list target matches no arm and fails at runtime. Appending | _ -> [] means “match failure (no candidates) when the target cannot be decomposed” and makes the arms exhaustive. The recognized exhaustive arm shapes are (1) a trailing wildcard arm, (2) the pair of [] and :: (complete for collections), and (3) a single irrefutable arm (such as $tgt).

6.12Types of Pattern Functions

Pattern functions, introduced in Section 2.9 of Chapter 2, are typed as well.

def pattern twin {a} (pat1: a) (pat2: [a]) : [a] :=
  (~pat1 & $x) :: #x :: ~pat2

In this definition, the parameter annotation (pat1: a) says “pat1 is a pattern matching values of type a”, and the result position : [a] says “the application is a pattern matching values of type [a]”. That is, the type of twin reads roughly as Pattern a -> Pattern [a] -> Pattern [a]. Argument patterns are checked at application sites.

matchAll [1, 2] as multiset integer with
  | twin ($y :: _) _ -> y
-- Type error: the first argument requires
--   Pattern Integer, but $y :: _ is Pattern [Integer]

For the admissibility check (Section 6.10), an application of a pattern function behaves as the skeleton of its body pattern. The body of twin is nested cons patterns, so a match expression using twin needs a matcher that can decompose cons (list or multiset). Conversely, a pattern function whose body is just a parameter imposes no structure of its own; only the demands of the argument patterns propagate. In this way, “which matchers this pattern needs” is tracked statically even through pattern functions.

6Defining Matchers

6.1inductive pattern Declaration

6.2Basics of Matcher Definitions

6.3Definition of the eq Matcher

Difference between something and eq.

6.4Definition of the multiset Matcher

6.5Definition of the sortedList Matcher