[Prev][Next][Index][Thread]
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