- Zena Ariola (Chair)
- Boyana Norris
- Michal Young
- Mark Lonergan
Truth and falsehood, questions and answers, construction and deconstruction; as Alcmaeon (510BC) once said, most things come in dual pairs. Duality is a guiding force, a mirror that reveals the new from the old via opposition. This idea appears pervasively in logic, where duality is expressed by negation that inverts "true" with "false" and "and" with "or." However, even though the theory of programming languages is closely connected to logic, this kind of strong duality is not so apparent in the practice of programming. For example, sum types (disjoint tagged unions) and pair types (structures) are related to dual concepts. But in the realm of programming, natural biases makes the duality between these two features difficult to see, much less use for any practical purpose.
To get a better understanding of the role that duality plays in programming, we take a radical shift of our viewpoint. Our approach is based on the philosophy known as the Curry-Howard isomorphism or proofs-as-programs paradigm which says that programs following a specification are the same thing as proofs for mathematical theorems. The Curry-Howard isomorphism gives a logical foundation for programming languages, especially functional ones, based on the connection between Gentzen's natural deduction system of logic and Church's lambda calculus core programming language.
Here, we will instead explore Gentzen's sequent calculus, a logic steeped in duality, as a model for computational duality. By applying the Curry-Howard isomorphism to the sequent calculus, we get a language that combines dual concepts in programming as equal-and-opposite partners: the data types found in functional languages are dual the co-data types (that is, interface-based objects) found in object-oriented languages, control flow is dual to information flow, induction is dual to co-induction. The foundation of the sequent calculus lets us come up with a duality-based semantics for reasoning about the behavior and safety of programs — as well as language-wide guarantees — which uses the idea of orthogonality: checking the safety and correctness of a pool of candidate implementations based on a comprehensive test suite.
We use the core languages derived from the sequent calculus to apply ideas from logic to issues that are relevant the compilation of programs. The idea of logical polarity — that types have either a "positive" or "negative" character based on the structure of their rules — shows us a small, symmetric basis of primitive programming constructs, which follow common algebraic and logical laws, that can faithfully represent of all user-defined data and co-data types. The "faithfullness" of encodings, meaning that the space of potential program behaviors before and after encoding are exactly the same, is crucial for the compilation process. We want to have complex structures in source programming language that are more convenient for the programmer, and complex structures in target language that are more efficient for implementation. But in the middle of a compiler, it would be better to only deal with only the minimum number of simple concepts for the purpose of program optimization and analysis.
We reflect this idea back into a core intermediate language for functional languages, at the cost of symmetry, by using the traditional canonical relationship between the sequent calculus and natural deduction. This relationship lets us derive a generalized lambda calculus with user-defined data and co-data equivalent to a restricted (intuitionistic) subset of the sequent calculus. We also show how to extend the lambda calculus and the relationship to cover the entire (classical) sequent calculus by bringing out the control-flow in functional programs, letting us share and name control the same way we share and name data. This extension enables a direct representation of join points, which are essential for tractable optimization and compilation, via first-class control.