Pattern Calculus

Barry Jay has recently published a book on the Pattern Calculus (which has been discussed before).

The pattern calculus is a new foundation for computation, in which the expressive power of functions and of data structures are combined within pattern-matching functions. The best existing foundations focus on either functions, as in the lambda-calculus, or on data structures, as in Turing machines, or on compromises involving both, as in object-orientation. By contrast, a small typed pattern calculus is able to support all the main programming styles, including functional, imperative, object-oriented and query-based styles, and there is evidence that it can support a language for Web services, able to exploit data structures about which almost nothing is known.

The book covers the operational semantics of both functional and OO features, as well as static and dynamic pattern-matching. Then it covers type systems necessary to deal with all the wild polymorphism thus gained - in rather readable fashion. Then it covers bondi, a programming language based on ML, Java and (lots of!) pattern-matching.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

A review

[Here part of the review of this book which I have sent to Computing Reviews; link to appear soon. Truncated to 300 characters by request of Computing Reviews.]

Programmers lucky enough to use a programming language featuring properly integrated pattern matching greatly value the expressivity gain. But as Barry Jay teaches us in ``Pattern Calculus'', we have barely started to properly explore the design landscape of pattern matching in programming languages. More than anyone else, he has systematically explored both the theory and practice of pattern matching.

More importantly, the knowledge thus gained has been largely transcribed into a lovely book. [...]

Link for the bondi language?

This looks interesting. Has anyone found a working link where one can download bondi? http://bondi.it.uts.edu.au/ doesn't work for me.

Bondi language homepage

That page works for me. And you should be able to download everything from here.

Indeed

Yeah, seems that the server is back online. (Or maybe there was a hiccup at my ISP.) Thanks for the heads up.

Other previous, related discussion

LtU archives: Shape Theory

Jacques' review of this book does not mention or place it within the context of Barry Jay's previous project on his theory of shapes. The pattern matching approach is meant to eventually support better research into Shape Theory. So, it can be viewed as a bootstrapping mechanism for other research efforts down the road.

Shape theory

I am aware of his previous work on shapes (rather liked it too). The review doesn't mention it because the book essentially doesn't either! There is a nice chapter on Functorial Polymorphism, but otherwise is silent on some of the really nice aspects of FISh. Barry Jay has posted on LtU before, hopefully he'll have more to say on this himself.

But you're right, a longer review could well mention FISh, and how bondi seems to be pursuing a somewhat different line of research. Hopefully these threads will rejoin in future work, as they seem complementary and probably even synergistic.

patterns and all that

Hi everyone,
a few comments here.

Thanks Jacques for the kind review.

My uni's web-site was down for maintenance over the weekend (very bad timing). Also, there was a glitch in the tar.ball for bondi (now fixed).

The pattern calculus is indeed related to shape theory. Patterns are a means of describing shapes or, more generally perhaps, structures. The biggest criticism of FISh was that its shapes were static. As bondi supports dynamic patterns, it would be interesting to persue it for dynamic shaper analysis.

Actually, bondi goes beyond pattern calculus in some ways. One is the ability to extend existing functions with new cases. For example, the function toString can have new cases added as new datatypes are declared.

Other related things I am working on can be found at http://www-staff.it.uts.edu.au/~cbj/Publications/latest.html

Yours,
Barry

Adaptive Software

Barry,

You might also be interested in Karl Lieberherr's work on Adaptive Object-Oriented Software. I've not seen you cite it, so I figured you might be completely unaware of it as related work.

As an aside, I first saw shape theory when I was looking for a disciplined way to manage memory in a language I was developing with pen and paper. This was in college when I was first learning what pointer analysis was, and what effect pointer aliasing had on things such as optimizing C compilers.

adaptive software

Yes, there are some connections. Inevitably, there are many related works not referenced in my book (it has 200 references, not 1000). The adaptive software approach is a form of meta-programming, whereas the pattern calculus is quite fundamental.

Nested Pattern

Hello Barry, in your paper "Pure pattern calculus" with Kesner, you essentially disallow nested patterns (you can form them syntactically, but nothing ever matches). You say "As defined, matching one [pattern matching] against another always fails. To do otherwise would require that matching be parametrised by yet another set of variables, representing those which are bound within the pattern itself, so is left for another occasion". I wonder if you have considered nested patterns since that paper.

case matching

Hi Martin,

we have looked at case matching from time to time but the results never satisfied. To match a case [theta] p -> s against another such [theta'] p' -> s' one must first align the bound symbols to ensure that theta = theta'. Then match p and p' and s and s'. This is fairly straightforward, except that one must check that symbols in theta are not in the range of the resulting match. However, there remain some technical difficulties.

I was not motivated to pursue them because it is against the theme of the book, that data structures and functions are different sorts of things, with patterns representing the former, and used to build the latter. Also, it didn't produce an exciting examples.

However, our latest work matches structures in general, not just data structures in a new form of combinatory logic, using combinators S and F. S is as usual, while F is for factorisation. This is written up in http://www-staff.it.uts.edu.au/~cbj/Publications/factorisation.pdf It supports factorisation of combinators, whether they represent functions or data structures.

I hope that this answers your question.
Barry