TypeScript Proposition as Types

pas.ts

// https://www.typescriptlang.org/play?#code/PTAEDMEMBsGcFNQAcBOB7JbYEsAu20A7UQUqIAoXATyUQBUUBXRAXlAcIGtC0B3QgbjJkQoXI0SoMWPAWKASogrVEAMRgJQrQvABu8FIOFgAItlgArdgGN8RUAEFQgCiJQAIUU1QAeRQAeOwBpXAD4NUDJQUAAfUABvUUgAcwAuUAAiaHhwXFT+UG0YJhSHAF8wiOi43ESU1JRsBIALbNz86ELXUGKDMnArG2IMrL8ggApW9rsAShTvP0CtXRQQmPDQFHhcBhRiSuq0wezA8cQusmKhXsJrWTX6pp8XUeOUl2mvXwW9QMfY1fXN7axeLJNJ1RqHPIFE6Cc49Po3eB4Bp6OauQIAYVGqzQKBmvgCwX82MIABlMrgUiNIEVJhoQuiiREiAAlO4U0AjABGL1pzHpRLe6N+fw2W2II1WTJQADoqgkNMxWOlyakyhF1QB+UBEMlZEY46XHWmS9UpFls-Uyo2rSYwoSGUDoogWK79eygQDkRK53Ig7IQACaon6sADaBJcAF1uiIAJIAWyQ0GwlkgbocAFoQm4qB540ggyFWFSaXTXAYRABRACODGwrXgV19oB8fO9OcQMfA4ALoRDeYLgX7LkCdiCUaEIgAcvAEqmbgBCOw+0CTtC4YahEYADxLrc++ntImU2BQsFwoFTuHgCfPuDQyHQ-oYlkQkBXM7nulESjhrpuUGwDJ-QAfS0BJgMva8kFwEZaRWVZLmuWxwBxHQUVHYt7Dgk1-jFCBUMWKlbVWUohAids0HAfD1kWVYRHVAA9DV7QiRC3X9NAGE5DJQJnYYRi7SkU2gaBOUgSwOEpaksNLfdeRCOSil+dVQBAE02JuHhIDwYCUJovRMKmFJ92UlS1lFQEtJ0vS0JQIjBBU2EVNwwEuxGKzcF0gi9GIiJznIpRKNADiuJ4sC6LARjmIiejsEQVd1wS4YgjI0AMnPaTCAYONOT0UIQu4+BeISEYOFLDgRgAVkmYjVnS0BuVALKcry1g3wAalAAAmO0JzAJ0UHWaxgs4wqmo-N04wYM8GokdBtGwf14H9URkQfNAEhQSA4zjbBCHlaBIH2hhEngMglssQ71ggeFbAKsK+Iw8AUiSpLRyCN47HLMAYyWwh8CoNLIB4d1WyXDTbEW-jpKmUyXOISBepEABlNA40QSw0bjWxJEo2BQD20ASQ25NfyQ4hrC3AtYNMtSAo8BKHFYN6ggMen4rXFxQiSx42dUgAqQWheFkXRbF0BfobAHKCJ4H8bFhXFZF4BUvohxnFUOBEBbEIlwiTHCBmxapbwShgMOnhgIARhSTtu1mAlNYQIIR0LUAQ1SmKwHV0AncQTN7BNEY7BxP35NARFcGROyQ5QP3AkWwJIE5WAthW1tk9TlB-UmIkTREDNdacX21DOlSiNLA4iMZUBxwi90vXoJhmzB1YDaNv7pfN4HgK622uz8ANUSb+AXfsN2Pfz73PVAEfQADvX1SpANw6O-0QwABgjPOVIL+ei8b8Qg8gcOQ0geYGBE7fVjrmKlfvh-H6fhWVbo5-FffWc3Qt+X34flWIj1xJMDbUVEo6IHgFuS6DAlorV2v6f0GR64+0XG3IgM1IHQNgcBeBiD4B4lRIzN2Jp7pFTAqVUsJoIgVTBE0KklCzLqgqlXE+kwqGgBqiaWqXsG6gEXPvEuWs0GG3PGBbuPBbYJkHoGAkRDAh+zdiMM+8w1x2AjOHbguA7D2WEH-PR+jH6vzvu-UARhEAAFkcSzkIAAcnxsAngv8DFiwAapMA85g7F1eC3EI-CvTzjcPrdB54lrYxQNY62-duxJQdt8IIY8-SBhZoEHm8SJ5Tz4Z45w3iA5+L4YEpeCVgKx28a2D2jCIgV1bEUkpIwWE1UCOwypnJw41JxC4EYtCYItLYYw6+jCRB5ICQIjxPtXjsKUZogkmjIzh2Du08Okdo7zJQMOJqqiVG4FeDXOu9dRkz28TrPhKCClHhxFpbOwUTzwHJpkhwXocm+JOcImaoSrFHS6rpHg-pJH5jekPcM8TAizEZikzm8TQirBGDUtepSUoqVIcVChrZ2HMPJPQlFFTQA0ItJyBhWKVxrmKbCpR58GrqKaRw3pZlOEqV8mqEQLhxIcAuStf01zbn8OcMM3JniHnUvbiE687zCCfM5N835PgQUbMJVsse-yZFxIhcwIOjMcQJThUHZR5L5LsKWQZSlaqUAaprowkYUyNGqOrpS81nNLVbK5Lndh9LAEvKFWE6xfcJYDwVQWMe0qtFgrlRPN54SPlfP9IEUNnrgLiv9BGN+zik3Jv5q-RN99QDVlrPWRsN0-y2AAGRsEILIJxBijFuPdAHLmRyuXeh4coc5kBLnsqGm6Tx1baQBxGHW8ZQSREQEIMBdgsgI2Sv7IC4FvhQXBGIeXSAXUWl0nYYi8hZVMUVLRXqN8G6sU4vBBKAl6oF2ciIpSiItKKmXrpXzRlzLWVXLbTcHtYyu0hA7VmAVwTB3DpLUQWNEqJZSIDZOoD+ZAVzvVFM4COJgJc13ce5dWL9V2XPesrRMGUBwdNRU21Wj7XaJPjhs1S7WycmI+qbhoBBU-pHf++AVYok+AnXEqdPgZ2PAnuAIddGh3gG+YEbjv7R1xoTbCe0QggA

// false proposition ⊥
type True = unknown;

// true proposition ⊤
type False = never;

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


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

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

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)
  );
}


// Conjunction A ∧ B
type And<A, B> = [A, B];


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

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

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


// First attempt to produce a Negative type
function failed_neg_attempt() {

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

  typeof forever
  //    ^?


  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);
  }
  typeof double_neg
  //    ^?
  //  ie Not<Not<A>>

  let a: number = double_neg(k => k(5));

  let b: number = a + 2;
}


// Correct double negation must be provided the programming language
declare function double_neg<A>(f: Not<Not<A>>): A;

// Identity law A => A
function id<A>(a: A) {
  return a;
}

// Some common proofs in Logic
function ctx<A, B>() {
  //
  type NotA = Not<A>;

  type NotB = Not<B>;

  /**************************** Identity Laws *****************************/

  //  A ∨ False <=> A
  const identity_law_1: Iff<Or<A, False>, A> = [

    // A ∨ False -> A
    (AorFalse) => either(AorFalse, id, absurd => absurd),

    // A -> A ∨ False
    (a) => left(a),
  ];

  // A ∧ True <=> A
  const identity_law_2: Iff<And<A, True>, A> = [

    // A ∧ True -> A
    (and) => and[0],

    // A -> A ∧ True
    (a) => [a, null],
  ];

  /********************************************************************/

  /************************ Negation laws *****************************/
  
  // Law of the excluded middle
  // A ∨ !A
  const excluded_middle: Or<A, NotA> = 
    double_neg(k => 
      k(right(a => 
        k(left(a))
      ))
    );

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

  /***************** De Morgan's Laws *****************************/
  // !(A ∨ B) <=> !A ∧ !B
  const demorgan_1: Iff<Not<Or<A, B>>, And<Not<A>, Not<B>>> = [
    // !(A ∨ B) -> !A ∧ !B
    (Not_AorB) => [
        (a) => Not_AorB(left(a)), 
        (b) => Not_AorB(right(b))
      ],
      // !A ∧ !B -> !(A ∨ B)
      ([notA, notB]) => (AorB) => either(AorB, notA, notB),
  ];


  // !(A ∧ B) <=> !A ∨ !B
  // Forward direction !(A ∧ B) -> !A ∨ !B
  const demorgan2_fwd: Imp<Not<And<A, B>>, Or<NotA, NotB>> = 
  (Not_AandB) =>
    double_neg(k => 
      k(left(a => 
        k(right(b => 
          Not_AandB([a, b])
        ))
      ))
    );
  
  // Backward direction !A ∨ !B -> !(A ∧ B)
  const demorgan2_bwd: Imp<Or<NotA, NotB>, Not<And<A, B>>> =
    (NotAorNotB) =>
    ([a, b]) =>
      either(
        NotAorNotB,
        (notA) => notA(a),
        (notB) => notB(b),
      );
    

  const demorgan2: Iff<Not<And<A, B>>, Or<NotA, NotB>> = [demorgan2_fwd, demorgan2_bwd]
  /********************************************************************/


  /************* Equivalence function & unions ***********************/

  // A -> B <=> !A ∨ B
  // Forward direction (A -> B) -> (!A ∨ B)
  const fn_union_fwd: Imp<Imp<A, B>, Or<NotA, B>> = 
    (a2b) =>
      double_neg(k => 
        k(left(a => 
          k(right(
            a2b(a)
          ))
        ))
      );

  // Backward direction (!A ∨ B) -> (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,
        );

  const fn_union_eq: Iff<Imp<A, B>, Or<NotA, B>> = [fn_union_fwd, fn_union_bwd]
}