16 November 2004 

4:00 - 5:30  Barry Jay (UTS, Sydney)
        
             The pattern calculus


Abstract

Pattern-matching algorithms can support more algorithms, and more
polymorphism, than previously realised. Standard approaches consider
patterns of the form c p1 ...pn where c is a constructor and p1 ... pn
are all patterns. Now the pattern \x \y (lambda x lambda y) can match
any compound data structure. For example, equality of data structures
can be defined using just two cases, one for atoms and one for
compounds. Again, one may consider patterns of the form x \y in which
x is a free variable. This can be replaced by a linear function
suitable for building patterns. The caclculus now supports
higher-order patterns so that patterns may be passed as parameters or
returned as results. This may simplify the manipulation of
semi-structured data, XML, etc. since whole ontologies could be passed
as parameters and then used to create patterns dynamically.

Typing of such powerful algorithms requires novel type derivation
rules. A key insight is that different cases in a patternmatch may
have different types, provided that they are all specialisations of a
common default type. Two forms of specialisation have been
identified. The first is by type variable instantiation. It allows one
to define map1 : (a->b) -> c a -> c b by cases whose types instantiate
the variable c to different type combinators. The second is by
(unifiable) subtyping which eliminates many of the difficulties
usually associated with subtyping. Further refinements are reuqired to
handle linear types.

Work to date has identified five distinct forms of polymorphism: data;
structure; path; pattern; and subtype. The resulting calculus has been
implemented sufficiently well to support demonstrations of all the key
ideas. The presentation will provide an overview of the pattern
calculus, going into details of types, terms and theorems if
appropriate.