"Proof in functions" by @mbrandonw implemented in JavaScript and using Flow as a static type checker

proof_in_functions.js

// @flow

/*

  "Proof in functions" by @mbrandonw
  implemented in JavaScript and using Flow as a static type checker

  Original post:
  http://www.fewbutripe.com/swift/math/2015/01/06/proof-in-functions.html

*/

type Empty = void & null;

export function f1 <A> (x: A): A {
  return x
}

export function f2 <A, B> (x: A, y: B): A { // eslint-disable-line no-unused-vars
  return x
}

export function f3 <A, B> (x: A, g: (a: A) => B): B {
  return g(x)
}

export function f4 <A, B, C> (g: (a: A) => B, h: (b: B) => C): (a: A) => C {
  return a => h(g(a))
}

type Or<A, B> = { type: 'LEFT', val: A } | { type: 'RIGHT', val: B };

export function f5 <A, B> (x: A): Or<A, B> {
  return { type: 'LEFT', val: x }
}

export function f6 <A, B, C> (x: Or<A, B>, g: (a: A) => C, h: (b: B) => C): C {
  switch (x.type) {
    case 'LEFT' :
      return g(x.val)
    case 'RIGHT' :
    default :
      return h(x.val)
  }
}

type Not<A> = (a: A) => Empty;

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

export function deMorgan1 <A, B> (f: Not<Or<A, B>>): And<Not<A>, Not<B>> {
  return [
    (a: A) => f({ type: 'LEFT', val: a }),
    (b: B) => f({ type: 'RIGHT', val: b })
  ]
}

export function deMorgan2 <A, B> (f: And<Not<A>, Not<B>>): Not<Or<A, B>> {
  return (x: Or<A, B>) => {
    switch (x.type) {
      case 'LEFT' :
        return f[0](x.val)
      case 'RIGHT' :
      default :
        return f[1](x.val)
    }
  }
}