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

@YBogomolov I'm not convinced though, looks like the following simpler encoding is working too, am I missing something?

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

import { identity } from 'fp-ts/lib/function'

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

export interface Leibniz<A, B> {
  (a: A): B
}

// ------------------------------------------
// 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: identity }
}

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

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

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

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

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

export function evaluate<A>(expr: Expr<A>): A {
  switch (expr.type) {
    case 'Add':
      return expr.proof(evaluate(expr.left) + evaluate(expr.right))
    case 'Mult':
      return expr.proof(evaluate(expr.left) * evaluate(expr.right))
    case 'Equal':
      return expr.proof(evaluate(expr.left) === evaluate(expr.right))
    case 'Not':
      return expr.proof(!evaluate(expr.expr))
    case 'Val':
      return 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

I'm sure you already figured it out, but if it is okay, I would like to leave a little note on it too.

Original article mentions that for efficiency sake coerce and Leibniz proofs are implemented with unsafeCoerce. However, there is also real implementation without cheating for efficiency. It seems to me that the difference between two examples is related to that. Isn't it the case?

@qlonik actually there's no unsafe coercion (i.e. a as any somewhere) in both the encodings.

This

-- no-cheating `coerce` implementation:

newtype Identity a = Identity a

unIdentity :: forall a. Identity a -> a
unIdentity (Identity a) = a

coerce :: forall a b. (a ~ b) -> a -> b
coerce p a = unIdentity (coe p (Identity a))

corresponds to this

import { URI } from 'fp-ts/lib/Identity'

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

I played a bit with the implementation, using Leibniz equality, identity and Getter from monocle as proof part.

IMO, everything is fine with a simpler implementation. When we specialize Expr with a concrete type, we naturally simplify Leibniz<A, B> into an identity (a: A) => A. When we pattern-match on expr.type, TypeScript does type narrowing for that case, expr.proof gets inferred into a conversion of that specific type into A, so everything remains well-typed.

Great job 👏

@gcanti After playing with these examples more I came with this implementation. I believe that's as close as we can get to Haskell's GADTs:

export type Expr<A> =
  | Add<A>
  | Mult<A>
  | Equal<A>
  | Not<A>
  | Val<A>;

class Add<A> {
  readonly _A!: A;
  readonly type: 'Add' = 'Add';
  constructor(readonly left: Expr<number>, readonly right: Expr<number>) {}
}

class Mult<A> {
  readonly _A!: A;
  readonly type: 'Mult' = 'Mult';
  constructor(readonly left: Expr<number>, readonly right: Expr<number>) {}
}

class Equal<A> {
  readonly _A!: A;
  readonly type: 'Equal' = 'Equal';
  constructor(readonly left: Expr<number>, readonly right: Expr<number>) {}
}

class Not<A> {
  readonly _A!: A;
  readonly type: 'Not' = 'Not';
  constructor(readonly expr: Expr<boolean>) {}
}

class Val<A> {
  readonly _A!: A;
  readonly type: 'Val' = 'Val';
  constructor(readonly value: number) {}
}

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

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?