University of Technology, Sydney

The Pattern Calculus

Pattern-matching algorithms can support more algorithms, and more polymorphism, than previously realized. 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 calculus 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 pattern match may have different types, provided that they are all specializations of a common default type. Two forms of specialization 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 required 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.

Host: Bob Harper

Appointments: Norene Mears

Principles
of Programming Seminars

Monday, November 15, 2004

3:30 p.m.

Wean Hall 4623