I have been interested, for many years, in what is generally called computational classical type theory (CCTT). The idea is to take some proof system for classical logic, and turn it into a programming language via the Curry-Howard isomorphism. Cut elimination or normalization for the proofs turns into reduction for the corresponding program terms. There is nothing at all objectionable about this, and indeed it is very interesting to see term notations for proofs of classical theorems like (Peirce’s Law) or . It was the brilliant insight of Griffin (my that POPL ’90 was a good one, as Lamping’s paper on optimal beta-reduction was that year, too) that proofs of such classical theorems essentially involve control operators like call-cc. This is all super cool and very interesting.

And I accept what I understand to have been David Hilbert’s position that non-constructive reasoning is an essential tool for mathematics, and that rigid constructivism (i.e., insisting on constructive proofs for every theorem) is thus disastrous for advancement of mathematics. In Computer Science at least, I have sometimes in the past thought that the ability to do things like case-split on whether a term in some unrestricted programming language terminates or not could be very helpful if not critical for verification of general programs.

Since Curry-Howard is great and applies very nicely to classical logic, and since classical logic is useful if not essential for certain kinds of verification, CCTT should be fantastic in my book, right?

No — and of course I will tell you why.

The problem is that the Curry-Howard isomorphism a reasonable programmer expects to hold is broken in CCTT. The problem can be seen clearly with disjunctions. Under Curry-Howard, a disjunction corresponds to a sum type . Given an element of such a sum, we can case split on whether that element is the injection of an element in or else in . And in doing so, we gain some actionable **information**. But this does not happen when we split on a use of the law of excluded middle (LEM). We gain no information at all in the two branches of the split. And indeed, the usual way CCTT proves LEM is to say (so to speak): it is which is true. Then if the branch of the split for the right disjunct ever tries to make use of that information — wait, how can it do that? The only thing you can do with the negative fact that is to apply it to a proof of to obtain a contradiction. And if you ever do that, the machinery of CCTT will take your proof of , backtrack to the point where it originally told you is true, and then invoke the branch of the split for the left disjunct, with that proof of . Super clever! (This is dramatized by a famous story about the devil told by Phil Wadler; see my old post about this.) But also, note that it means you can never take action based on the result of such a case split. Everything must be indefinitely revisable, due to the possible need to backtrack. So you cannot split on an instance of LEM and print 1 in the first branch and 2 in the second. Or rather, you can, but the meaning is not at all what you expect. “This Turing machine either halts or it doesn’t.” We case split on this, and could easily think that we are gaining some information by doing so. But we are not. Your code will just always print 2. This is not what you reasonably expect under the Curry-Howard interpretation of disjunctions. And thus using CCTT for programming is not a good idea.

It would be fine to use classical reasoning for *reasoning* about programs. For the justification of some property of a program might require (or be easier with) some non-constructive case split. But the program itself should not do such things, or else the abstraction Curry-Howard seems to offer us is violated.

Is this an argument against sum types in the presence of control operators? (Genuine question)