Pattern calculus

{{More footnotes|date=November 2016}}

Pattern calculus bases all computation on pattern matching of a very general kind. Like lambda calculus, it supports a

uniform treatment of function evaluation. Also, it allows functions to be

passed as arguments and returned as results. In addition, pattern calculus supports

uniform access to the internal structure of arguments, be they pairs

or lists or trees. Also, it allows patterns to be passed as arguments and

returned as results. Uniform access is illustrated by a

pattern-matching function {{code|size}} that computes the size of an

arbitrary data structure. In the notation of the programming language

bondi, it is given by the recursive function

let rec size =

| x y -> (size x) + (size y)

| x -> 1

The second, or default case {{code|x -> 1}} matches the pattern {{code|x}}

against the argument and returns {{code|1}}. This

case is used only if the matching failed in the first case. The

first, or special case matches against any compound, such

as a non-empty list, or pair. Matching binds {{code|x}} to the left component

and {{code|y}} to the right component. Then the body of the case adds the

sizes of these components together.

Similar techniques yield generic queries for searching and updating. Combining recursion and decomposition in this way yields path polymorphism.

The ability to pass patterns as parameters (pattern polymorphism) is illustrated by defining a

generic eliminator. Suppose given constructors {{code|Leaf}} for creating

the leaves of a tree, and {{code|Count}} for converting numbers into

counters. The corresponding eliminators are then

elimLeaf = | Leaf y -> y

elimCount = | Count y -> y

For example, {{code|elimLeaf (Leaf 3)}} evaluates to {{code|3}} as does {{code|elimCount (Count 3)}}.

These examples can be produced by applying the generic eliminator

{{code|elim}} to the constructors in question. It is defined by

elim = | x -> | {y} x y -> y

Now {{code|elim Leaf}} evaluates to | {y} Leaf y -> y which is equivalent to {{code|elimLeaf}}. Also {{code|elim Count}} is equivalent to {{code|elimCount}}.

In general, the curly braces {{code|{} }} contain the bound variables of the

pattern, so that {{code|x}} is free and {{code|y}} is bound in | {y} x y -> y.