Propositions as types correspondance (PAT) (or Types as Propositions) is one of the most intriguing discoveries of Computer Science. The gist of it is:

• In Logic land, you often see stuff like P is True. Here, P can stand for some statement that can be true or false. And a Proof is constructed to back the statement.
• In code, we've got something like: let x: T = term;.

The correspondance is basically saying Logic and Programming are two sides of the same coin:

• In Logic: When you claim something is true, you must provide a Proof for it.
• In code: If you got a type and want to use it, you create a term of that type.

It's as if we were writing let x: P = proof; in TypeScript. And it's not just some quirky coincidence. If we restrict ourself to a pure subset TypeScript, you'll see you can write logical proofs using code.

Code's Take on Logic Constructs

First let's review quickly the key concepts in Logic, they work pretty much like the booleans we use in programming:

• True or ⊤: This represents a proposition that's always true.
• False or ⊥: signifies something that's never true.
• A ∨ B : A disjunction. True if either A or B hold true. Could be both.
• A ∧ B : A conjunction. Both A and B must be true.
• A -> B : Logical implication. If A is true, then B is consequently true.
• !A : negation, a Proposition that's true if A is not.

There's also A <=> B. It's essentially stating that A implies B and B implies A. In other words, (A -> B) ∧ (B -> A).

Now for each one of the above constructs we have an equivalent type in Typescript.

True corresponds to any inhabitated type

type True = unknown;

We could use a singleton type like null or undefined. But with the unknown type, we can assign any value to it.

False translates to an uninhabited type in TypeScript. This mirrors the fact that there's no proof for a false proposition in Logic:

type False = never;

A ∨ B corresponds to a discriminated union type in TypeScript.

type Or<A, B> = 
  | { tag: "left"; value: A } 
  | { tag: "right"; value: B };

We'll also write two constructor functions:

function left<A>(value: A): Or<A, never> {
  return { tag: "left", value };
}

function right<B>(value: B): Or<never, B> {
  return { tag: "right", value };
}

And a helper for case analysis:

function either<A, B, C>(
  or: Or<A, B>,
  onLeft: (a: A) => C,
  onRight: (b: B) => C,
): C {

  return (
    or.tag === "left" 
      ? onLeft(or.value) 
      : onRight(or.value)
  );
}

A ∧ B corresponds to a pair of types:

type And<A, B> = [A, B];

Logical implications translate to function types:

type Imp<A, B> = (a: A) => B;

Finally, The equivalence A <=> B corresponds to a pair of 2 functions. It's a sort of 2-way conversion between A and B

type Iff<A, B> = [Imp<A, B>, Imp<B, A>];

So far, everything's been kinda familiar, right? But with negation, things are getting a bit wild.

Negative types

Let's start by unpacking the meaning of False/never. The never type acts as a universal subtype, as it can be assigned to any other type.

You might wonder about the meaning of any here. Intriguingly, any stands as a proposition that is both True and False at once. This duality allows any value to be assigned to it, making it akin to unknown or True. On the flip side, it can fit into any type (except never), reflecting the nature of never or False.

In logical discourse, a proposition that holds as true and false simultaneously is labeled a contradiction. If one can prove a contradiction, the whole logic system just falls apart.

In a parallel sense, being able to produce terms of type any compromises the soundness of the type system. As highlighted in the TypeScript documentation, the flexibility of any sacrifices type safety.

This brings us to the concept of Proof by contradiction: To disprove a proposition A (or to assert !A), one assumes A is true and then demonstrates that this assumption leads to a contradiction.. In essence, !A equates to A -> False.

Hence, negating a type A in TypeScript translates to the function (x: A) => never.

type Not<A> = (x: A) => never;

Double negation, paradoxes and the halting problem

Constructing a term of type A -> never poses challenges though. How can we return a never value when, by definition, never lacks any values?

One way to produce a negative type in Typescript is by writing a non terminating function. For example:

function forever<A>(a: A) {
  return forever(a);
}
// typeof forever = <A>(a: A) => never

Typesript detects that the function never terminates and assigns to it a type of <A>(a: A) => never. (There are alternative methods to create functions that don't return, but remember we're operating within a limited TypeScript subset here).

Is this type designation genuinely accurate from a logical standpoint?

Consider the following function

function double_neg<A>(ff: (callback: (a: A) => never) => never): A {
  //
  function wait_forever(a: A): never {
    return wait_forever(a);
  }

  return ff(wait_forever);
}

A closer look at the type reveals it corresponds to Not<Not<A>> => A. This is just the double negation law in Logic: !!A = A.

The implementation exploits the fact that never can be assigned to any type A. Now we should be able to use our double negation in our code to turn values of type !!A into values of type A:

const a = double_neg(k => k(5));

let b = a + 2;
// ...

However an issue arises: the statement let b = a + 2; is never reached. Upon entering double_neg, the body invokes k(5) where k represents the non terminating function wait_forever. The program remains trapped there indefinitely.

The core issue with wait_forever is its endless recursion. It's like an infinite loop that keeps running without an exit condition. In Logic, infinite loops can give birth to tricky paradoxes, like this classic:

This statement is false

This is the essence of the liar paradox. If you try to reason through it, you'll get stuck in a endless cycle of contradictions. Give it a try!

1. If we assume that statement is true, then the statement must be false as it claims to be. But then it contradicts our own assumption that the statement was true.a

2. If we assume that statement is false, then it's ironically being truthful about its falsehood, making it true. Again, this is a contradiction because we just assumed it was false.

The self-referencing nature of the statement is the real troublemaker here. It creates a loop where the truth value keeps toggling between true and false, never settling, similar to how a piece of code is stuck in an infinite loop.

This is bad for Logic, which requires every proof to be finite. What this says in reality is that wait_forever is not exactly the function we're seeking for our negative types.

A more Logic freindly interpretation of negation is actually possible, and would allow writing programs in double negation style. To see how, let's revisit our earlier example:

const a = double_neg(k => k(5));

let b = a + 2;
// ...

The double negation principle, !!A = A, hints that the program should progress beyond the initial line, assigning a number type to a. Which number? In this context, 5 seems like a logical choice.

But then, what's the role of the k argument, and how do we instantiate it?

Here's the twist: k isn't a function we can implement by ourselves. It has to be provided to us by the programming language.

This isn't just a normal function, It belongs to a special class known as continuations. Think of a continuation as a snapshot of a program's future from a particular moment. For example, consider this code:

// assume f : (n: number) => number
const a = f(5);

let b = a + 2;
// ...

Now, let's transform it into a continuation-passing style (CPS):

f(5, (a) => {

  let b = a + 2;
  // ...
})

In the CPS style, every function receives an extra k argument, which represents the program's subsequent steps.

Our double_neg, by converting from Not<Not<A>> to A, essentially transforms a CPS function call into a standard value of type A. It achieves this by encapsulating the program's future steps and repackaging them into a function awaiting a value to proceed.

While non-terminating functions and continuations both return never, continuations avoid embedding self-referential inconsistencies within our system. By the time the function concludes, the program has also concluded.

That means to make values of type Not<A>, our programming language should equip us with something to encapsulate the program's subsequent steps as a continuation.

Although TypeScript doesn't natively support this construct, for the sake of discussion, let's pretend it does:

declare function double_neg<A>(f: Not<Not<A>>): A;

While the double negation principle might feel intuitive, I should mention it's not something universally accepted. Some logicians believe that just because a statement isn't proven doesn't mean the opposite holds true. Think of it as "absence of evidence isn't evidence of absence." This viewpoint is held by intuitionistic logic.

In contrast classical Logic embraces the double negation law. But as we've observed, to embed this principle in a programming language, we need a control operator to turn double negation into identity. This hints at a deep connection between the context in which a program runs and the foundational logic underpinning it.

If you've dabbled with Lisp-like languages (like Scheme or Clojure), you might've bumped into a cousin of double_neg named call/cc (though its type is a bit different).

Diving into Logical Proofs using TypeScript

Having established a bridge between Logic's concepts and our TypeScript subset, We're ready to weild this knowledge to perform some common proofs in Logic.

The most elementary proof is the tautology A => A. This is just the identity function

function id<A>(a: A) {
  return a;
}

Let's see some more interesting proofs.

We'll define all our proofs in a generic function, to abstract over propostions A and B.

function context<A, B>() {
  //
  type NotA = Not<A>;

  type NotB = Not<B>;

  // ... subsequent proofs will be populated here
}

Law of Excluded Middle (A ∨ !A <=> True)

The law of excluded middle is a foundational principle in classical logic, which asserts that any proposition is either true or its negation is true. There's no in-between state.

Let's first write the implementation:

// A ∨ !A
const excluded_middle: Or<A, NotA> = 
  double_neg(k => 
    k(right(a => 
      k(left(a))
    ))
  );

To construct a value of type A ∨ !A, we have 2 choices:

1. Constructing A: Creating an instance of an arbitrary type A is unfeasible. It's like attempting to materialize something from nothing.

2. On the other hand, creating an instance of !A is feasible. To understand this, recall that !A is synonymous with a continuation of type (a:A) -> never. So we'll need the help of double_neg.

Here's the step-by-step breakdown of the implementation:

1. Invoke double_neg and capture the current continuation as k.
2. Inside the continuation, the next plausible action is to make use of right to indicate we're choosing the negation path. This gives: k(right(a => _)).
3. Now, inside our function (a => _), we need to return a value of type never. The one tool we have at our disposal to achieve this effect is the captured continuation k. Since we now have access to a value of type A (through the function argument), we can use k to redirect our flow to the other branch, i.e., left(A). This is expressed as: k(left(a)).

This construction can look mind-bending, especially if encountered for the first time. It's somewhat analogous to a closed time-like loop in physics, where cause and effect blur.

In [one of his papers (https://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf), Philipe Wadler, illustrates the above behavior:

The following story illustrates this behavior. (With apologies to Peter Selinger, who tells a similar story about a king, a wizard, and the Philosopher’s stone.)

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b)
I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available? “I accept,” said the man at last. “Do I get (a) or (b)?” The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realized that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!” The devil took possession of the valise. Then he said, “Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

Lastly, an important takeaway is that the double_neg function anchors this logic in the domain of classical logic. In intuitionistic logic, which is more conservative about claims of truth or falsity, such a construction might not hold true. Here, if you cannot furnish a proof for A, it doesn't automatically mean A is false. It simply means that the truth value of A remains undetermined.

A ∧ !A -> False

A proposition and its negation cannot both be true simultaneously.

// A ∧ !A -> False
const neg_law: Imp<And<A, NotA>, False> = ([a, notA]) => notA(a);

In code, this means we can just smash matter and antimatter together and watch them annihilate.

Equivalence between Functions and Discriminated Unions?

Here's a thought-provoking equivalence:

A -> B <=> !A ∨ B

It basically says a function A -> B is equivalent to an union of a continuation expecting A and a value B.

Let's see what this means in code.

From (A -> B) to (!A ∨ B):

// Transition from (A -> B) to (!A ∨ B)
const fn_union_fwd: Imp<Imp<A, B>, Or<NotA, B>> = 
  (f) =>
    double_neg(k => 
      k(left(a => 
        k(right(
          f(a)
        ))
      ))
    );

Utilizing the previous time-traveling maneuver, we initially yield a continuation to solicit an A type. Then we use our A -> B function to transform the A into a B value. Subsequently, we reinvoke the continuation to yield the result B to the surroundings.

Conversely, for the transformation of a union type to a function:

// Transition from (!A ∨ B) to (A -> B)
const fn_union_bwd: Imp<Or<NotA, B>, Imp<A, B>> = 
  notA_or_B => 
    a =>
      either(
        notA_or_B,
        (notA) => notA(a),
        (b) => b,
      );

To morph a union type to a function, we assume an A argument. Then based on the content of our container !A ∨ B:

• If it's a continuation waiting for an A, we just present our A argument.
• Conversely, if it's a B value, we directly return it.

This may appear as a form of trickery. One usually expects a genuine mechanism to turn an A into a B. Instead, the transformation feels more like routing around the union, merely forwarding existing information rather than truly processing it.

To be honest, I don't really have a plausible explanation. I was thinking it might be because of classical logic quirks, but the above proof doesn't use double_neg so it's equally valid in intuitionistic logic.

I tried to ask my freind GPT-4. Can't say it adds much but here's the answer anyway:

"Imagine you have a box that might either contain a machine that needs some input A to work or an already finished product B. Now, if someone hands you an A, this function simply checks the box. If there's a machine (notA), it feeds the A to it. If there's a finished product B, it just hands it over. The function doesn't do the "creation" part itself, but instead relies on what's in the box. This doesn't feel like a trick anymore; it's more about delegation and routing based on what's available."

TS playground where you can find other common proofs in Logic.

Happy proving!