An old and celebrated analogy says that writing programs is like proving theorems. This analogy has been productive in both directions, but in particular has demonstrated remarkable utility in driving progress in programming languages, for example leading towards a better understanding of concepts such as abstract data types and polymorphism. One of the best known instances of the analogy actually rises to the level of an isomorphism: between Gentzen's natural deduction and Church's lambda calculus. However, as has been recognized for a while, lambda calculus fails to capture some of the important features of modern programming languages. Notably, it does not have an inherent notion of evaluation order, needed to make sense of programs with side effects. Instead, the historical descendents of lambda calculus (languages like Lisp, ML, Haskell, etc.) impose evaluation order in an ad hoc way.
This thesis aims to give a fresh take on the proofs-as-programs analogy---one which better accounts for features of modern programming languages---by starting from a different logical foundation. Inspired by Andreoli's focusing proofs for linear logic, we explain how to axiomatize certain canonical forms of logical reasoning through a notion of pattern. Propositions come with an intrinsic polarity, based on whether they are defined by patterns of proof, or by patterns of refutation. Applying the analogy, we then obtain a programming language with built-in support for pattern-matching, in which evaluation order is explicitly reflected at the level of types---and hence can be controlled locally, rather than being an ad hoc, global policy decision. As we show, different forms of continuation-passing style (one of the historical tools for analyzing evaluation order) can be described in terms of different polarizations. This language provides an elegant, uniform account of both untyped and intrinsically-typed computation (incorporating ideas from infinitary proof theory), and additionally, can be provided an extrinsic type system to express and statically enforce more refined properties of programs. We conclude by using this framework to explore the theory of typing and subtyping for intersection and union types in the presence of effects, giving a simplified explanation of some of the unusual artifacts of existing systems.
Successfully defended April 17, 2009!
4 comments:
Congratulations, and happy post-doc in Paris/PPS! Pierre-Louis Curien spoke highly of your work during a proof theory course.
Bravo docteur.
Great Thesis!
One question: Given your insights into polarized logic, if you had to create a practical language - what would it look like, and what features would it have that doesn't exist in ML/Haskell or languages based on CBPV?
thanks A. and pingouin for the well wishes. Pal-Kristian, yes, that's the ultimate question, and I think I'd have to do a lot more hacking before I could come up with good answers. But I have some ideas. The most basic (that comes directly from polarized logic) is just that a language should allow programmers to define both positive and negative types, by describing their constructors or destructors. And that pattern-matching should be available not only for eliminating positive types (as usual in ML/Haskell), but also for introducing negative types. The latter can also be seen as typed control operators -- in my thesis I only describe undelimited control, but I believe the approach extends pretty nicely to delimited control operators, which seem to be of more practical value.
There's a lot of other areas in type theory where I think polarity and focusing can be useful concepts for simplifying and extending existing approaches, particularly to better account for effects and equality. My thesis works through the theory of refinement types. I think there is something to be said about dependent types and type abstraction as well.
Post a Comment