The Pattern Calculus

Typing branching constructs

b : bool s:T t:T
--------------------
if b then s else t:T

Notice that there is only one type parameter (T) to be shared by three terms b,s,t.

However, in a pattern-matching term or extension

at p use s else t

there are three types to be considered: that of the pattern p, the specialisation s to be returned when the pattern is matched, and the default t to be used when matching fails. So a more expressive rule should take the form

p:P s:S t:T
----------------------
at p use s else t: ???

where ??? is some type created from P,S and T.

In the usual treatments, every pattern must have exactly the same type, and so ??? is both T and P->S. However, the term s need only be typed in a richer context in which matching has occured, so the type P->S may be more specialised than T.

The rest of this note indicates how two apparently different research problems, the creating and typing generic functional programs and the typing of object-oriented programs, can both be tackled in the same term calculus, the pattern calculus, by using different forms of type specialisation. In the former case it is by type substitution. In the latter case it is by sub-typing, and perhaps type substitution.

The Pattern Calculus

p ::= x | c | p p
s,t ::= x | c | t s | at p use s else t

where x is a variable, c is a constructor and t s is an application. The expressive power of the calculus is determined by the choice of patterns. Consider these examples:

at x use s else t
at True use s else t
at Cons x1 (Cons x2 x3) use else t
at x1 x2 use s else t

The first corresponds to the lambda-abstraction \x.s since a variable matches with anything. The second is a form of conditional which when applied to True it returns s. The third pattern matches with lists whose length is at least 2. The fourth pattern matches with any data structure such as (Cons x1) x2 or (Pair x1) x2 but not with a reducible function application such as (at p use s else t) u.

The reduction rules for the pattern calculus are given by rules for matching: with a variable corresponds to beta-reduction; with a constructor corresponds to the standard conditional; and with an application p1 p2 reduces to matching against p1 and then against p2.

Specialisation by type substitution

p:P s:upsilon R t:Q -> R
---------------------------- upsilon = mgu(P,Q)
at p use s else t: Q -> R

where upsilon is the most general unifier of P and Q. For example, one can define an equality function of type X -> X -> bool with different cases for integers, floats, pairs, lists, etc. Of course, the etc. is a little unsatisfactory. Better is to replace this ever-expanding list of cases by a structurally polymorphic program (or generic functional program) in which a finite list of cases covers all possibilities as described in The Pattern Calculus .

Specialisation by sub-typing

p:P s:S t:Q->R
-------------------------------- P < Q and S < R
at p use s else t: P->S /\ Q->R

where P->S /\ Q->R is a form of intersection of the types P->S and Q->R.

For example, consider a class Point of points with a method

move :Float -> Point

which, in sub-class of CPoint of coloured points is to have type

move: Float -> CPoint.

Let t : Point -> Float -> Point be a function representing m and let p be a pattern representing a coloured point which is used to define a function s:Float -> CPoint representing m in class CPoint. Then m can be represented by

at p use s else t : CPoint -> Float -> CPoint /\ Point -> Float -> Point Details of this approach to objects, and that of the following heading, can be found in Methods as pattern-matching functions

Specialisation by both type substitution and sub-typing

p:P s:S t:Q->R
-------------------------------- upsilon = mgu'(P,Q)
at p use s else t: P->S /\ Q->R S < upsilon R

This approach can be used to model inheritance by parametric polymorphism; the coloured points can be used to illustrate.

Represent the class Point by the type Point X for some type variable X so that move has type

move : Point X -> Float -> Point X

Now represent the class CPoint by the type Point (CPoint Y). The type for move on coloured points

move : Point (CPoint Y) -> Float -> Point (CPoint Y)

is obtained by instantiating the type parameter X to be CPoint Y.

Conclusion

FISh2