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

That is true, there is no explicit cast or unsafeCoerce being used.

I remember reading this issue on typescript issue tracker, where they talked about "return-only generics" and dangers associated with them: microsoft/TypeScript#33272. To be fair, in the issue they talked about TS3.5, and I'm not sure if situation has changed for later versions. In one of the posts, one of the contributors mentioned that in some cases they might act as a "hidden" cast. Do you think it might apply here?