-
-
Save gcanti/9a0c2a666621f03b80457831ff3ab997 to your computer and use it in GitHub Desktop.
// 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 |
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?
@qlonik actually there's no unsafe coercion (i.e. a
as any
somewhere) in both the encodings.This
corresponds to this