[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