Polarity in Type Theory by Robert Harper.
From the post:
There has recently arisen some misguided claims about a supposed opposition between functional and object-oriented programming. The claims amount to a belated recognition of a fundamental structure in type theory first elucidated by Jean-Marc Andreoli, and developed in depth by Jean-Yves Girard in the context of logic, and by Paul Blain-Levy and Noam Zeilberger in the context of programming languages. In keeping with the general principle of computational trinitarianism, the concept of polarization has meaning in proof theory, category theory, and type theory, a sure sign of its fundamental importance.
Polarization is not an issue of language design, it is an issue of type structure. The main idea is that types may be classified as being positive or negative, with the positive being characterized by their structure and the negative being characterized by their behavior. In a sufficiently rich type system one may consider, and make effective use of, both positive and negative types. There is nothing remarkable or revolutionary about this, and, truly, there is nothing really new about it, other than the terminology. But through the efforts of the above-mentioned researchers, and others, we have learned quite a lot about the importance of polarization in logic, languages, and semantics. I find it particularly remarkable that Andreoli’s work on proof search turned out to also be of deep significance for programming languages. This connection was developed and extended by Zeilberger, on whose dissertation I am basing this post.
The simplest and most direct way to illustrate the ideas is to consider the product type, which corresponds to conjunction in logic. There are two possible ways that one can formulate the rules for the product type that from the point of view of inhabitation are completely equivalent, but from the point of view of computation are quite distinct. Let us first state them as rules of logic, then equip these rules with proof terms so that we may study their operational behavior. For the time being I will refer to these as Method 1 and Method 2, but after we examine them more carefully, we will find more descriptive names for them.
Best read in the morning with a fresh cup of coffee (or whenever you do your best work).
Can’t talk about equivalence without types. (Well, not interchangeably.)