How do continuations represent negations (under the Curry–Howard correspondence)?

Question

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the Cartesian product is logical conjunction.)

Negation is represented as $A \to \bot$, where $\bot$ is the empty type. This works because if a type is inhabited, there can't be any function $A \to \bot$ (if you do you have such a function and the type is inhabited, feed the value into it and you get an element of the empty type, hence a contradiction), and vice versa (if $A$ is empty, the empty function $A \to \bot$ exists).

But once you add continuations to your language, an $A$-continuation can also be given the type $A \to \bot$. (see e.g. the symmetric lambda calculus). This apparently provides computational meaning to classical theorems; for example, the $\mathcal{C}$-operator (a basic operator for manipulating continuations), has type $\neg\neg A \to A$.

But can't you have continuations for non-empty types? If you add continuations, does $\neg A$ no longer express "$A$ is-empty/is-false/has-no-proofs"? It can't, right? This formulation makes an inhabitant of $\mathbb{N} \to \bot$ axiomatic, and $\mathbb{N}$ certainly isn't uninhabited. So what does "$\neg A$" actually express, if not "$A$ is-empty/is-false/has-no-proof"? And how do you actually express "$A$ is-empty/is-false/has-no-proof" when continuations exist?

Answer 1

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type is held abstract, it works a lot like 'false' in that there is no introduction rule for it.

With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression $e : +\mathsf{int}$ and reduce that expression to a numeral $n$. This means that the continuation $\bullet : ¬int$ is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually $\mathsf{int}$, because we are interested in using continuation-based computations that eventually result in integers. $\bullet$ is something that immediately completes the computation, hence the rules:

$$(begin)\ \ \ \ e : +int \leadsto \langle e | \bullet \rangle$$ $$(end)\ \ \ \ \langle n | \bullet \rangle \leadsto n$$

I don't know what happens if you have $\bullet$ involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.

Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.

In that setting, $⊥$ is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also $0$, which gets the principle of explosion (which is arguably the distinct part of the empty type¹). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom $⊥$ is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).

Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.

1. In the continuation-with-abstract-result-type setting, you can also interpret explosion, but it has sort of a different meaning. Effectively such interpretations are always 'delimited' somewhere, even if it's only the end of your program. Explosion means that if you somehow get a value of the abstract result type, you can throw away your current continuation and jump to the delimiter. So it is an 'abort' operation. Linear logic doesn't allow this; all continuations must be used (and used exactly once), so explosion must be justified by involving an 'impossible' situation, like having a value of an empty type.

Answer 2

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for any formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of the logic (i.e. if $A ⊢ B$ then $\overline{B} ⊢ \overline{A}$) and forms a Boolean sub-logic, associated with a Boolean sub-lattice of the Heyting lattice. The $\overline{∧}$ of the sub-logic corresponds to the $∨$ of the original logic since you have the equivalence $$\overline{A}\overline{∧}\overline{B} = (A → X)∧(B → X) ⊣⊢ A∨B ⊃ X = \overline{A∨B}.$$ But the $\overline{∨}$ need not correspond to $∧$ of the original logic, since you only have $$\overline{A}\overline{∨}\overline{B} = (A → X)∨(B → X) ⊢ A∧B ⊃ X = \overline{A∧B}.$$ Nevertheless, the $\overline{A}$ form a Boolean sub-logic. Negation corresponds to $\overline{¬}\overline{A} = \overline{A} → X$, and the double negative rule applies, since you have the equivalence $$\overline{A} = A → X ⊣⊢ ((A → X) → X) → X = \overline{¬}\overline{¬}\overline{A}.$$ The $⊢$ direction is a special case of the inference $$b ⊢ (b → c) → c,$$ while the $⊣$ direction is a special case of the inference $$b → d ⊣ ((b → c) → c) → d.$$

So, continuations can refer broadly to any $X$, not just to $⊥$. The mapping $A$ into $\overline{\overline{A}}$ is then a forward map of the original logic into a Boolean-sublogic, while the $\overline{A}$ map into "responses" for the $\overline{\overline{A}}$. This is laid out in detail at the very outset of Classical logic, continuation semantics and abstract machines, J. Functional Programming 8 (6): 543–572, November 1998, which is open access at the link. You can get a clearer (and more accurate) picture there, than what I laid out in my brief description here.

Answer 3

The type of a function (lambda) is the type of its argument and the type of what it returns. Some functions do not return anything - they go into an infinite loop or in some theories raise an error, and thus their return type is empty. It's not that their return type is null (or unit type, or really they are procedures). It's that they never return anything and any potential capture of their result value will never happen.

Continuations are, for all practical purposes, infinite loops. They never return anything and thus their return type is void. Waiting for them to finish will take forever.

Now you can modify your theory slightly. You may say that when a continuation receives a special value from the void type, it finishes and returns null, for instance. This does not affect the definition of a continuation. The continuation will still never return, because this value from the void type does not exist. However, the type of continuation behaves as negation from now. When you feed a value from non-empty type, the continuation loops forever. When you feed it a hypothetical value from a void type, it returns null, which is non-empty.

You could make it a little bit less hypothetical if you introduce a special "error" value. The use of this value is forbidden, that means when you use it, an error happens (compare it to throwing an exception). Now "empty type" does not mean "looping forever" but "raising an error, failing to finish normally". You define a continuation in such a way that when they encounter an error, they quit gracefully returning a normal value.

Now when you feed the continuation a normal value, they would loop forever, as expected. When you feed them the "error" value, they encounter an error the moment they try to use it and exit, returning a value.

Again, this works as a type negation. Here "false type" does mean "a type without any non-error value". This could be a valid theory for a language featuring weak pointers (like C) where the "error" value is a null pointer. You can define some void type without any normal value but you still can make a null pointer to that type, where dereferencing always fails. (Side note: "void" in C doesn't mean a "false type" but unit type actually.)

The key point is that you can always extend your theory with some axiom that says: when we receive a value from the empty type, something happens. This is always compatible with the theory, as this can never happen, yet it can serve some theoretical purposes.