Skip to content

Instantly share code, notes, and snippets.

@zaach
Last active November 26, 2020 22:10
Show Gist options
  • Save zaach/f85443e9ed5d210bf5d7b0191c5c2058 to your computer and use it in GitHub Desktop.
Save zaach/f85443e9ed5d210bf5d7b0191c5c2058 to your computer and use it in GitHub Desktop.
Compute the Ackermann function using TS types
// Natural Numbers
interface Zero {
isZero: true;
}
interface Successor<N extends Nat> {
prev: N;
isZero: false;
}
type Nat = Zero | Successor<Nat>;
// Helpers
type One = Successor<Zero>;
type Two = Successor<One>;
type Three = Successor<Two>;
type Four = Successor<Three>;
type Five = Successor<Four>;
type Six = Successor<Five>;
type Seven = Successor<Six>;
type Eight = Successor<Seven>;
type Nine = Successor<Eight>;
type Ten = Successor<Nine>;
type Eleven = Successor<Ten>;
// Operators
type Pred<N extends Nat> = N extends Successor<infer U> ? U : Zero;
type Add<N1 extends Nat, N2 extends Nat> = N1 extends Zero
? N2
: N1 extends Successor<infer U>
? Successor<Add<U, N2>>
: never;
type Times<N1 extends Nat, N2 extends Nat> = N1 extends Zero
? N1
: N2 extends Successor<infer U2>
? Successor<N1 extends Successor<infer U1> ? Add<U2, Times<U1, N2>> : never>
: Zero;
type Sub<N1 extends Nat, N2 extends Nat> = {
0: N1;
1: N2 extends Successor<infer U> ? Sub<Pred<N1>, U> : never;
}[N2 extends Zero ? 0 : 1];
// Ackermann Function
// This uses explicit boxing/unboxing on the second argument to fly under TS's circular reference radar.
type Acker<M extends Nat, N extends Nat> = FlattenBox<Acker_<M, Box<N>>>;
type Acker_<M extends Nat, N extends Box<any>> = M extends Zero
? Box<Successor<FlattenBox<N>>>
: M extends Successor<infer PM>
? FlattenBox<N> extends Zero
? Box<Acker_<PM, Box<One>>>
: FlattenBox<N> extends Successor<infer PN>
? Box<Acker_<PM, Acker_<M, Box<PN>>>>
: never
: never;
// Another version of Ackermann that uses an explicit Continuation Passing Style. TS types don't have
// first class "functions", so we pass closure data around in a nested data structure
type AckerCPS<M extends Nat, N extends Nat> = Acker_Tail<M, N, Closure<Zero, Nil>>;
type Acker_Tail<
M extends Nat,
N extends Nat,
Fr extends Closure<Nat, Frame>
> = M extends Zero
? Fr extends Closure<infer ClosureM, infer LastClosure>
? LastClosure extends Closure<Nat, Frame>
? Acker_Tail<ClosureM, Successor<N>, LastClosure>
: Successor<N>
: never
: M extends Successor<infer PM>
? N extends Zero
? Acker_Tail<PM, One, Fr>
: N extends Successor<infer PN>
? Acker_Tail<M, PN, Closure<PM, Fr>>
: never
: never;
type Frame = Nil | Closure<Nat, Frame>;
interface Closure<M extends Nat, Past extends Frame> {
m: M;
prev: Past;
}
// Utils
interface Box<T> {
val: T;
}
type FlattenBox<T> = {
0: never;
1: T extends Box<infer U> ? FlattenBox<U> : T;
}[T extends object ? 1 : 0];
// This cleaner alternative works in TS >= 4.1.x
//type FlattenBox<T> = T extends Box<infer U> ? FlattenBox<U> : T
// helper that flattens and subtracts one
type PredFlattenBox<NB extends Box<any>> = FlattenBox<NB> extends Successor<
infer U
>
? Box<U>
: Box<Zero>;
// Hyperoperation, a version of the Ackermann function that can perform +,x,^, ect. operations
type Hyper<N extends Nat, A extends Nat, B extends Nat> = FlattenBox<
Hyper_<N, A, Box<B>>
>;
type Hyper_<N extends Nat, A extends Nat, B extends Box<any>> = N extends Zero
? Box<Successor<FlattenBox<B>>>
: FlattenBox<B> extends Zero
? N extends One
? Box<A>
: N extends Two
? Box<Zero>
: N extends Successor<Nat>
? Box<One>
: never
: Box<Hyper_<Pred<N>, A, Hyper_<N, A, PredFlattenBox<B>>>>;
// Tests
// Simple operators
type TestAdd2And3 = Add<Two, Three>;
type TestAdd1And0 = Add<One, Zero>;
type TestAdd0And2 = Add<Zero, Two>;
type TestSub = Sub<Zero, Two>;
type TestSub2 = Sub<Two, Two>;
type TestSub3 = Sub<Five, Two>;
type TestSub4 = Sub<Five, Zero>;
type TestMul = Times<Four, Two>;
type TestMul2 = Times<Zero, Two>;
type TestMul3 = Times<Two, Zero>;
type TestMul4 = NatToDecimal<Times<Ten, Eleven>>;
// Ackermann Function
type TestAcker00 = Acker<Zero, Zero>; // 1
type TestAcker01 = Acker<Zero, One>; // 2
type TestAcker10 = Acker<One, Zero>; // 2
type TestAcker11 = Acker<One, One>; // 3
type TestAcker12 = Acker<One, Two>; // 4
type TestAcker21 = Acker<Two, One>; // 5
type TestAcker22 = Acker<Two, Two>; // 7
type TestAcker23 = Acker<Two, Three>; // 9
type TestAcker24 = Acker<Two, Four>; // 11
type TestAcker31 = NatToDecimal<Acker<Three, One>>; // 13
type TestAckerCPS00 = AckerCPS<Zero, Zero>; // 1
type TestAckerCPS01 = AckerCPS<Zero, One>; // 2
type TestAckerCPS10 = AckerCPS<One, Zero>; // 2
type TestAckerCPS11 = AckerCPS<One, One>; // 3
type TestAckerCPS12 = AckerCPS<One, Two>; // 4
type TestAckerCPS21 = AckerCPS<Two, One>; // 5
//type TestAckerCPS22 = AckerCPS<Two, Two>; // 7 (too much recursion error)
// Hyperoperation
// Test base cases
type TestHyper0 = Hyper<Zero, Two, Two>; // b + 1 if n = 0 -> 3
type TestHyper1 = Hyper<One, Two, Zero>; // a if n = 1 and b = 0 -> 2
type TestHyper2 = Hyper<Two, Two, Zero>; // 0 if n = 2 and b = 0 -> 0
type TestHyper3 = Hyper<Three, Two, Zero>; // 1 if n >= 3 and b = 0 -> 1
type TestHyper3b = Hyper<Four, Two, Zero>; // 1 if n >= 3 and b = 0 -> 1
// Test operators
type TestHyperAdd = Hyper<One, Two, Three>; // H1(2, 3) = 2 + 3 = 5
type TestHyperTimes = Hyper<Two, Two, Three>; // H2(2, 3) = 2 * 3 = 6
type TestHyperExponent = Hyper<Three, Two, Three>; // H3(2, 3) = 2^3 = 8
type TestHyperTetration = NatToDecimal<Hyper<Four, Two, Three>>; // H4(2, 3) = 2^2^2 = 16
// Check value
const five: TestAcker21 = {
isZero: false,
prev: {
isZero: false,
prev: {
isZero: false,
prev: {
isZero: false,
prev: {
isZero: false,
prev: {
isZero: true,
},
},
},
},
},
};
// Pretty print natural numbers as number literal
const fiveDecimal: NatToDecimal<TestAcker21> = 5;
// Pretty Print Utils
type Unshift<U extends any[], T extends any> = ((
a: T,
...t: U
) => void) extends (...t: infer R) => void
? R
: never;
type NatToDecimal<
N extends Nat,
__acc extends { state: NatToTupleResult<Nat, any[]>; done: boolean } = {
state: NatToTupleResult<N, []>;
done: false;
}
> = {
0: NatToDecimal<N, NatToUnaryTuple_<__acc["state"], 1, []>>;
1: __acc["state"]["tuple"]["length"];
}[__acc["done"] extends true ? 1 : 0];
type NatToUnaryTuple<
N extends Nat,
Fill extends any = 1,
__acc extends { state: NatToTupleResult<Nat, any[]>; done: boolean } = {
state: NatToTupleResult<N, []>;
done: false;
}
> = {
0: NatToDecimal<N, NatToUnaryTuple_<__acc["state"], Fill, []>>;
1: __acc["state"]["tuple"];
}[__acc["done"] extends true ? 1 : 0];
// Trampoline
type NatToUnaryTuple_<
T extends NatToTupleResult<Nat, any[]>,
Fill extends any = 1,
NumberOfBounces extends any[] = []
> = {
2: { state: NatToTupleResult<T["nat"], T["tuple"]>; done: false };
0: { state: NatToTupleResult<T["nat"], T["tuple"]>; done: true };
1: T["nat"] extends Successor<infer U>
? NatToUnaryTuple_<
NatToTupleResult<U, Unshift<T["tuple"], Fill>>,
Fill,
Unshift<NumberOfBounces, any>
>
: never;
}[T["nat"] extends Successor<Nat>
? NumberOfBounces["length"] extends 5
? 2
: 1
: 0];
interface NatToTupleResult<L, T> {
nat: L;
tuple: T;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment