[TYPES] ....pattern matching

[Barry Jay]

Speaking of pattern matching,

it is more than just a convenience. By allowing any term to be a 
pattern, one can obtain new forms of polymorphism that allow generic 
queries (updating, searching, etc) to treat query parameters as 
arguments, and to apply queries to arbitrary data structures. A pure 
(untyped) version of pattern calculus was presented at ESOP last month 
(joint work with Delia Kesner). An overview and various papers 
(including an improved version of pure calculus) can be found at   
http://www-staff.it.uts.edu.au/~cbj/patterns/

The terms of the pure pattern calculus are given by

t ::= x  |  t t  |   t -->_theta  t

where p -->_theta s is a case with pattern p, body s and binding 
variables theta. The only reduction rule is the match rule, which 
generalises beta reduction. 

A typed version of the pattern calculus able to support the five forms 
of polymorphism identified will be available shortly. It will use fairly 
conventional types (System F plus type applications and some constants) 
but novel type derivation rules for handling the extension of a function 
with a new case.  Further work would be required to integrate this into 
a version suitable for handling dependent types etc. along the lines 
suggested by Yong Luo.

Yours,
Barry Jay



Yong Luo wrote:

>[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>Since many have come to discuss partially defined functions and pattern
>matching after I gave the talk in TYPES2006 last week.
>
>There is a new version you can download from my home page if you are
>interested. Comments and suggestions are welcome.
>
>http://www.cs.kent.ac.uk/people/staff/yl41/TPF.ps
>
>Yong
>==============================
>Dr. Yong Luo
>Computing Laboratory
>University of Kent
>
>  
>