Posted on Sep 23 Propositions as types correspondance (PAT) (or Types as Propositions) is one of the most intriguing discoveries of Computer Science. The gist of it is:The correspondance is basically saying Logic and Programming are two sides of the same coin: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.First let's review quickly the key concepts in Logic, they work pretty much like the booleans we use in programming: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 typeWe 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:A ∨ B corresponds to a discriminated union type in TypeScript.We'll also write two constructor functions:And a helper for case analysis:A ∧ B corresponds to a pair of types:Logical implications translate to Function types:Finally, The equivalence A B corresponds to a pair of 2 functions. It's a sort of 2-way conversion between A and BSo far, everything's been kinda familiar, right? But with negation, things are getting a bit wild.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.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:Typesript detects that the function never terminates and assigns to it a type of (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 functionA closer look at the type reveals it corresponds to Not> => 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: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 falseThis 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!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.aIf 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: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:Now, let's transform it into a continuation-passing style (CPS):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> 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, 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: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).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 functionLet's see some more interesting proofs.We'll define all our proofs in a generic function, to abstract over propostions A and B.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:To construct a value of type A ∨ !A, we have 2 choices:Constructing A: Creating an instance of an arbitrary type A is unfeasible. It's like attempting to materialize something from nothing.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: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 proposition and its negation cannot both be true simultaneously.In code, this means we can just smash matter and antimatter together and watch them annihilate.Here's a thought-provoking equivalence:A -> B !A ∨ BIt 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):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:To morph a union type to a function, we assume an A argument. Then based on the content of our container !A ∨ B: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!Templates let you quickly answer FAQs or store snippets for re-use. Are you sure you want to hide this comment? It will become hidden in your post, but will still be visible via the comment's permalink. Hide child comments as well Confirm For further actions, you may consider blocking this person and/or reporting abuse Sven Cowart - Sep 22 Alexey Poimtsev - Sep 22 Enoch - Sep 22 Summerbud - Sep 22 Once suspended, yelouafi will not be able to comment or publish posts until their suspension is removed. Once unsuspended, yelouafi will be able to comment and publish posts again. Once unpublished, all posts by yelouafi will become hidden and only accessible to themselves. If yelouafi is not suspended, they can still re-publish their posts from their dashboard. Note: Once unpublished, this post will become invisible to the public and only accessible to Yassine Elouafi. They can still re-publish the post if they are not suspended. Thanks for keeping DEV Community safe. Here is what you can do to flag yelouafi: yelouafi consistently posts content that violates DEV Community's code of conduct because it is harassing, offensive or spammy. Unflagging yelouafi will restore default visibility to their posts. DEV Community — A constructive and inclusive social network for software developers. With you every step of your journey. Built on Forem — the open source software that powers DEV and other inclusive communities.Made with love and Ruby on Rails. DEV Community © 2016 - 2023. We're a place where coders share, stay up-to-date and grow their careers.