Skip to content

Instantly share code, notes, and snippets.

@gcanti
Last active September 23, 2022 10:55
Show Gist options
  • Save gcanti/9a0c2a666621f03b80457831ff3ab997 to your computer and use it in GitHub Desktop.
Save gcanti/9a0c2a666621f03b80457831ff3ab997 to your computer and use it in GitHub Desktop.
Approximating GADTs in TypeScript
// 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
@qlonik
Copy link

qlonik commented Feb 29, 2020

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?

@gcanti
Copy link
Author

gcanti commented Feb 29, 2020

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

@YBogomolov
Copy link

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 👏

@YBogomolov
Copy link

YBogomolov commented Feb 29, 2020

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

@qlonik
Copy link

qlonik commented Feb 29, 2020

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment