There is an interesting class of operations that make sense for arbitrary data structures but do not apply to functions. Examples include equality, searching, updating and mapping. However, the lambda-calculus, being a theory of functions, is unable to handle them in a uniform way. The pattern calculus [1] does so by using constructors to build data structures which are handled by pattern-matching functions. The main goal of this talk is to define sound type derivation rules which are able to reveal the polymorphism of the examples above.
The terms (meta-variables s,t,u) of the pattern calculus are
s,t,u ::= x | λx | a | t u | p→s∧t
where x is a free variable, λx the corresponding binding variable (lambda x), a is a constant (constructor or operator), t u is an application of t to u and p→s∧t is the extension whose pattern is p, whose body is s and whose default is t. Such an extension may be thought of as the addition of a new case or specialisation p→s to the default function t. In the simplest scenario, the type P→S of the specialisation and the type Q->T of the default are the same. More generally, the specialisation may have a specialised type so that
P→S < Q→T.
Specialisation may involve both type variable instantiation (as in parametric polymorphism) and also subtyping. For example, it arises if P→S < Q→T or there is a substitution σ such that P→S = σ(Q→T) or even if P→S < σ(Q→T).
Type specialisation allows the constructor calculus (a fragment of the pattern calculus) to support both data polymorphism (a.k.a. parametric polymorphism) and inclusion polymorphism. By allowing patterns of the form λx λy which are able to match any compound data structure, the static pattern calculus is able to support the path polymorphism used to define equality (by traversing all paths through compound structures). By allowing free variables in patterns, as in λy, the dynamic pattern calculus is able to support the pattern polymorphism used to manipulate data within unknown structures, e.g. as defined by XML schema. If there is time, I will revisit a fifth form of polymorphism, structure polymorphism used to support examples such as mapping and folding.