Approximating GADTs in TypeScript

GADT.ts

// Adapted from http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/

import { Kind, URIS } from 'fp-ts/lib/HKT'
import { URI } from 'fp-ts/lib/Identity'
import { identity } from 'fp-ts/lib/function'

// ------------------------------------------
// Leibniz
// ------------------------------------------

export interface Leibniz<A, B> {
  <F extends URIS>(fa: Kind<F, A>): Kind<F, B>
}

export function coerce<A, B>(proof: Leibniz<A, B>): (a: A) => B {
  return a => proof<URI>(a)
}

export function id<A>(): Leibniz<A, A> {
  return identity
}

// ------------------------------------------
// Expr
// ------------------------------------------

export type Expr<A> =
  | {
      readonly type: 'Add'
      readonly left: Expr<number>
      readonly right: Expr<number>
      readonly proof: Leibniz<number, A>
    }
  | {
      readonly type: 'Mult'
      readonly left: Expr<number>
      readonly right: Expr<number>
      readonly proof: Leibniz<number, A>
    }
  | {
      readonly type: 'Equal'
      readonly left: Expr<number>
      readonly right: Expr<number>
      readonly proof: Leibniz<boolean, A>
    }
  | {
      readonly type: 'Not'
      readonly expr: Expr<boolean>
      readonly proof: Leibniz<boolean, A>
    }
  | {
      readonly type: 'Val'
      readonly value: number
      readonly proof: Leibniz<number, A>
    }

export function add(left: Expr<number>, right: Expr<number>): Expr<number> {
  return { type: 'Add', left, right, proof: id<number>() }
}

export function mult(left: Expr<number>, right: Expr<number>): Expr<number> {
  return { type: 'Mult', left, right, proof: id<number>() }
}

export function equal(left: Expr<number>, right: Expr<number>): Expr<boolean> {
  return { type: 'Equal', left, right, proof: id<boolean>() }
}

export function not(expr: Expr<boolean>): Expr<boolean> {
  return { type: 'Not', expr, proof: id<boolean>() }
}

export function val(value: number): Expr<number> {
  return { type: 'Val', value, proof: id<number>() }
}

// ------------------------------------------
// evaluate
// ------------------------------------------

export function evaluate<A>(expr: Expr<A>): A {
  switch (expr.type) {
    case 'Add':
      return coerce(expr.proof)(evaluate(expr.left) + evaluate(expr.right))
    case 'Mult':
      return coerce(expr.proof)(evaluate(expr.left) * evaluate(expr.right))
    case 'Equal':
      return coerce(expr.proof)(evaluate(expr.left) === evaluate(expr.right))
    case 'Not':
      return coerce(expr.proof)(!evaluate(expr.expr))
    case 'Val':
      return coerce(expr.proof)(expr.value)
  }
}

// ------------------------------------------
// examples
// ------------------------------------------

// const value1: number
const value1 = evaluate(val(42))
console.log(value1) // 42

// const value2: number
export const value2 = evaluate(add(val(1), val(2)))
console.log(value2) // 3

// const value3: boolean
export const value3 = evaluate(equal(val(0), val(1)))
console.log(value3) // false

// const value4: boolean
export const value4 = evaluate(not(equal(mult(val(10), val(1)), add(val(0), val(1)))))
console.log(value4) // true