# pattern-matching: a new approach

```Announcing the availability of a new report titled

The Constructor Calculus

from

http://www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps

The *constructor calculus* is a variant of the lambda-calculus that
supports generic programming of functions for mapping, folding,
equality, addition, etc. based on fresh approach to data types, their
constructors, and pattern-matching.

Pattern-matching is usually interpreted by a case analysis in which
each pattern has the same type. Generic programming must combine a
variety of specialised functions into a single whole. This is achieved
in the constructor calculus by a new branching construct, the
*extension*

under c apply f else g

in which the branches f and g may have different types. Its evaluation
rules are:

under c apply f else g to c t1 ... tn  -> f t1 ... tn
under c apply f else g to t -> g t  (if t cannot be constructed by c)

f is the *specialisation function* which is to be applied to terms
constructed by c and g is the *default function*. The typing rule for
extensions is obtained by adding context information to

c: forall Delta.T_1 -> ... -> T_{n+1}     g:T-> T'
u = mgu(T_{n+1},T) 			    f:  u(T_1 -> ... T_n -> T')
---------------------------------------------------------------------
under c apply f else g:T-> T'

where c is a constructor with given type scheme forall Delta.T_1 ->
... -> T_{n+1} and u is the most general unifier of T_{n+1} and T. The
key point is that the type of f may be more specialised than that of g
since it need only act on terms constructed by c.

Such flexibility is essential if one is to define generic functions by
pattern-matching. Another requirement is a finite set of constructors
with which arbitrary data types may be represented. Two of the key
examples are inspired by combinatory logic, namely

evr : X -> KXY
rep : G(X,FX) -> SGFX

This requires support for higher types like S and also for pairs (and
tuples) of types like (X,FX). The use of pairing as a primitive allows
for the separation of the types representing data from those
representing structure; this is important for defining mapping etc.

This is all handled in a *combinatory type system*.  The raw syntax of
its kinds, types, type schemes and terms of the constructor calculus
are given by

k ::= a | * | (k,k) | k -> k
T ::= X | D | (T,T) | T T | T -> T
tau ::= T::* | forall a. tau | forall X::k. tau
t ::=   x
| d
| t t
| \x.t
| let x=t in t
| fix(\x.t)
| under t apply t else t

A detailed account of the system, including proofs of subject
reduction, Church-Rosser and a type inference algorithm may be found
in the paper. Examples of generic programs are also given. Feedback
would be appreciated.

Yours,
Barry Jay

--
Associate Professor C.Barry Jay,      Phone: (61 2) 9514 1814
Associate Dean (RPP), Faculty of IT   www-staff.it.uts.edu.au/~cbj
University of Technology, Sydney.     CRICOS Provider 00099F
```