3
$\begingroup$

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?

$\endgroup$
6
$\begingroup$

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 type1). 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.
$\endgroup$
  • $\begingroup$ While the second part of the answer looks speculative, there is indeed an interpretation in the same area as the first linked paper based on linear (involutive) negation. See Girard, A new constructive logic: classical logic (1991). Its continuation semantics is given by attributing to continuations an entirely different role than representing negation. $\endgroup$ – gadmm Jun 18 at 22:27
  • $\begingroup$ Oh, another paper to look at is Linear Logic for Constructive Mathematics, which gives an interpretation of classical linear logic in terms of intuitionistic logic that is (I think) different than what you'll find in Girard's paper. Contrary to the title, the semantics are not exactly linear, but it still has some similar distinctions. $\endgroup$ – Dan Doel Jun 19 at 0:52
-3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Okay, let me see if I understand, In Haskell, non-termination and errors are semantically equivalent; there is the one "undefined" element, ⊥. (To avoid confusion with void, I'm going to call void $0$.) So constructing a non-⊥ element of $A\to 0$ proves that $A$ has no non-⊥ elements. Are you saying that with continuations, non-termination is different from ⊥? Because continuations are defined (they aren't semantically $\bot$), but they don't terminate? And for $x:A\to 0$ to prove $A$ has no terminating elements, $x$ needs to be not just non-⊥, but also terminating, correct? $\endgroup$ – greatBigDot Jun 13 at 14:55
  • $\begingroup$ Also, there are things like Agda and Idris and Coq where every program terminates (unless certain pragmas or compilation flags are given). Under that system an element $x : A \to 0$ really does prove that $A$ is empty; no caveats about "non-⊥" are necessary. It sounds like that kind of totality impossible if you have continuations in your language, yes? $\endgroup$ – greatBigDot Jun 13 at 14:57
  • $\begingroup$ The statement "Continuations are [...] infinite loops" is deeply misleading. A better way of thinking about continuations is as return channel or jump (with values). See H. Thielecke's Continuations, functions and jumps, or, even better, R Milner's https://hal.inria.fr/inria-00075405/document. $\endgroup$ – Martin Berger Jun 14 at 8:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.