[TYPES] ....pattern matching
cbj at it.uts.edu.au
Tue Apr 25 19:51:00 EDT 2006
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
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.
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.
>Dr. Yong Luo
>University of Kent
More information about the Types-list