Proof that TypeScript's Type System is Turing Complete

main.md

type StringBool = "true"|"false";


interface AnyNumber { prev?: any, isZero: StringBool };
interface PositiveNumber { prev: any, isZero: "false" };

type IsZero<TNumber extends AnyNumber> = TNumber["isZero"];
type Next<TNumber extends AnyNumber> = { prev: TNumber, isZero: "false" };
type Prev<TNumber extends PositiveNumber> = TNumber["prev"];


type Add<T1 extends AnyNumber, T2> = { "true": T2, "false": Next<Add<Prev<T1>, T2>> }[IsZero<T1>];

// Computes T1 * T2
type Mult<T1 extends AnyNumber, T2 extends AnyNumber> = MultAcc<T1, T2, _0>;
type MultAcc<T1 extends AnyNumber, T2, TAcc extends AnyNumber> = 
		{ "true": TAcc, "false": MultAcc<Prev<T1>, T2, Add<TAcc, T2>> }[IsZero<T1>];

type _0 = { isZero: "true" };
type _1 = Next<_0>;
type _2 = Next<_1>;
type _3 = Next<_2>;
type _4 = Next<_3>;
type _5 = Next<_4>;
type _6 = Next<_5>;
type _7 = Next<_6>;
type _8 = Next<_7>;
type _9 = Next<_8>;

type Digits = { 0: _0, 1: _1, 2: _2, 3: _3, 4: _4, 5: _5, 6: _6, 7: _7, 8: _8, 9: _9 };
type Digit = 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9;
type NumberToType<TNumber extends Digit> = Digits[TNumber]; // I don't know why typescript complains here.

type _10 = Next<_9>;
type _100 = Mult<_10, _10>;

type Dec2<T2 extends Digit, T1 extends Digit>
	= Add<Mult<_10, NumberToType<T2>>, NumberToType<T1>>;



type Stack = EmptyStack | NonEmptyStack;
interface NonEmptyStack { prev: any, isEmpty: "false", item: any };
interface EmptyStack { isEmpty: "true" };

type IsEmpty<TStack extends Stack> = TStack["isEmpty"];
type Push<TItem, TStack extends Stack> = { prev: TStack, item: TItem, isEmpty: "false" };
type Peek<TStack extends NonEmptyStack> = TStack["item"];
type Pop<TStack extends NonEmptyStack> = TStack["prev"]; 
type PeekOrDefault<TStack extends Stack, TDefault> = {
	"true": TDefault,
	"false": Peek<TStack>
}[IsEmpty<TStack>];
type PopIfNotEmpty<TStack extends Stack> = {
	"true": TStack,
	"false": Pop<TStack>
}[IsEmpty<TStack>];


type TapeLike = { left: Stack, current: any, right: Stack, default: string }
type Left<TTape extends TapeLike> = TTape["left"];
type Right<TTape extends TapeLike> = TTape["right"];

type ConfigLike<TAutomata> = { state: keyof TAutomata, tape: TapeLike, halt: StringBool };
type AutomataLike = {
	[state: string]: {
		[symbol: string]: InstructionLike;
	}
};

type InstructionLike = { write: string, move: "r" | "_" | "l", next: string, halt: StringBool };

type NextConfig<TAutomata extends AutomataLike, TConfig extends ConfigLike<TAutomata>> 
	= NextConfig1<TConfig, TAutomata[TConfig["state"]][TConfig["tape"]["current"]]>;
type NextConfig1<TConfig extends ConfigLike<any>, TNextInstruction extends InstructionLike> 
	= NextConfig2<TConfig["tape"], TNextInstruction["write"], TNextInstruction>;
type NextConfig2<TTape, TWrite, TNextInstruction extends InstructionLike> = {
	state: TNextInstruction["next"],
	halt: TNextInstruction["halt"],
	tape: {
		"r": {
			left: Push<TWrite, Left<TTape>>,
			current: PeekOrDefault<Right<TTape>, TTape["default"]>,
			right: PopIfNotEmpty<Right<TTape>>,
			default: TTape["default"]
		},
		"_": {
			left: Left<TTape>,
			current: TWrite,
			right: Right<TTape>,
			default: TTape["default"]
		},
		"l": {
			left: PopIfNotEmpty<Left<TTape>>,
			current: PeekOrDefault<Left<TTape>, TTape["default"]>,
			right: Push<TWrite, Right<TTape>>,
			default: TTape["default"]
		}
	}[TNextInstruction["move"]]
}

type Simplify<T> = { [TKey in keyof T]: T[TKey] }

type Run<TAutomata, TConfig extends { halt: StringBool }, TSteps extends AnyNumber> = {
	true: TConfig,
	false: { false: Run<TAutomata, Simplify<NextConfig<TAutomata, TConfig>>, Prev<TSteps>>, true: TConfig }[IsZero<TSteps>]
}[TConfig["halt"]];

type RunUnbound<TAutomata, TConfig extends { halt: StringBool }> = {
	true: TConfig,
	false: RunUnbound<TAutomata, Simplify<NextConfig<TAutomata, TConfig>>>
}[TConfig["halt"]];

type InitialConfig = { state: "0", halt: "false", tape: { left: EmptyStack, current: "0", right: EmptyStack, default: "0" } };

type BusyBeaver4State = {
	"0": {
		"0": { write: "1", move: "r", next: "1", halt: "false" },
		"1": { write: "1", move: "l", next: "1", halt: "false" },
	},
	"1": {
		"0": { write: "1", move: "l", next: "0", halt: "false" },
		"1": { write: "0", move: "l", next: "2", halt: "false" },
	},
	"2": {
		"0": { write: "1", move: "r", next: "2", halt: "true" },
		"1": { write: "1", move: "l", next: "3", halt: "false" },
	},
	"3": {
		"0": { write: "1", move: "r", next: "3", halt: "false" },
		"1": { write: "0", move: "r", next: "0", halt: "false" },
	},
}

type S9 = Run<BusyBeaver4State, InitialConfig, _9>;

Honestly, I think it's more impressive if you run it with a state machine which actually terminates quickly:

type BusyBeaver2State = {
  "0": {
    "0": { write: "1", move: "r", next: "1", halt: "false" },
    "1": { write: "1", move: "l", next: "1", halt: "false" },
  },
  "1": {
    "0": { write: "1", move: "l", next: "0", halt: "false" },
    "1": { write: "1", move: "r", next: "0", halt: "true" },
  }
};

type BB2Result = Run<BusyBeaver2State, InitialConfig, _9>;

const x: BB2Result = {
  halt: "true",
  state: "0",
  tape: {
    current: "1",
    default: "0",
    left: {
      isEmpty: "false",
      item: "1",
      prev: {
        isEmpty: "false",
        item: "1",
        prev: { isEmpty: "true" }
      }
    },
    right: {
      isEmpty: "false",
      item: "1",
      prev: { isEmpty: "true" }
    }
  }
};

And you can verify the expanded state, too, since it doesn't take 107 steps. You can actually (in reasonable time), see completion information for everything in the shape of the result state, too. Super neat.

Hi, nice to hear from you again, I hope you are doing well @ Microsoft! :)
Sadly, my approach won't work any more soon (#14837) and typescript does something that requires non-linear time for linear recursion (the 4 state BB becomes much faster if you introduce new types for all the intermediary steps).
However, recursions through type members cannot be disallowed, as they are substantial: interface Foo { bar: Foo; }.
It would be super cool, if typescript had support for open generic types. This would make the following possible:

type Iterate1<TFunc<>, TBase> = TFunc<TBase>
type Iterate2<TFunc<>, TBase> = TFunc<Iterate1<TBase>>
...
type Iterate100<TFunc<>, TBase> = TFunc<Iterate99<TBase>>

These types could be auto generated and used like this:

type Next<T> = ...
const x: Iterate100<Next, Setup<BusyBeaver2Automata, BusyBeaver2State>>

This always terminates and can be used to do reasonable cool stuff.

And just recently, I discovered a new, much more usable device:

type N0_ = {};
type N1_ = N0_ & { "_1": never };
type N2_ = N1_ & { "_2": never };

interface N0 { clear: N0_; next: N1; };
interface N1 { clear: N1_; value: "_1"; next: N2; prev: N0; };
interface N2 { clear: N2_; value: "_2"; prev: N1; };

type Next<N extends { next: any }> = N["next"];
type Prev<N extends { prev: any }> = N["prev"];
type Value<N extends { value: any }> = N["value"];

type PushField<T extends { state: { next: any, clear: any } }, TFieldType> =
	((T | T["state"]["clear"]) 
	& { [TKey in T["state"]["next"]["value"]]: TFieldType }) & { state: T["state"]["next"] };

type PopField<T extends { state: { prev: any, clear: any } }> =
	T & T["state"]["prev"]["clear"] & { state: T["state"]["prev"] };

type Simplify<T> = { [TKey in keyof T]: T[TKey] }

type Empty = { state: N0 };
type S1 = Simplify<PushField<Empty, "Test1">>;
type S2 = Simplify<PushField<S1, "Test2">>;
type S3 = Simplify<PopField<S1>>;

const x: S3;
x.

Maybe this enables type subtraction somehow.

with TS template literal types, there's a very direct way to represent the tape now

// STRING MANIPULATION TOOLS
type First<T extends string> = T extends `${infer U}${string}` ? U : ''
type RemoveFirst<T extends string> = T extends `${string}${infer U}` ? U : ''

type Reverse<U extends string> = U extends ''
  ? ''
  : U extends '1' | '0'
  ? U
  : `${Reverse<RemoveFirst<U>>}${First<U>}`

type Last<T extends string> = First<Reverse<T>>
type RemoveLast<T extends string> = Reverse<RemoveFirst<Reverse<T>>>

// TAPE DATA STRUCTURE
type Tape = {left: string; current: string; right: string}

// TRANSITIONS
type MoveLeft<T extends Tape> = {
  left: `${T['left']}${T['current']}`
  current: First<T['right']>
  right: RemoveFirst<T['right']>
}

type MoveRight<T extends Tape> = {
  left: RemoveLast<T['left']>
  current: Last<T['left']>
  right: `${T['current']}${T['right']}`
}

type Write<T extends Tape, Value extends '0' | '1'> = {
  left: T['left']
  current: Value
  right: T['right']
}

// STATES
// program is 3 state busy beaver
type StateA<T extends Tape> = T['current'] extends '1'
  ? StateC<MoveLeft<T>>
  : StateB<MoveRight<Write<T, '1'>>>

type StateB<T extends Tape> = T['current'] extends '1'
  ? StateB<MoveRight<T>>
  : StateA<MoveLeft<Write<T, '1'>>>

type StateC<T extends Tape> = T['current'] extends '1'
  ? Halt<MoveRight<T>>
  : StateB<MoveLeft<Write<T, '1'>>>

type Halt<T extends Tape> = `${T['left']}${T['current']}${T['right']}`
type Start = {left: ''; current: ''; right: ''}

// RESULTS
type Result = StateA<Start>
// type Result = "111111"

see here for a typescript playground link

I am amazed this works!

Nice job @ricokahler.
Small mistake (not a big deal) I think the moveLeft and moveRight are opposite, this is should be the right form:

type MoveLeft<T extends Tape> = {
  left: RemoveLast<T['left']>
  current: Last<T['left']>
  right: `${T['current']}${T['right']}`
}

type MoveRight<T extends Tape> = {
  left: `${T['left']}${T['current']}`
  current: First<T['right']>
  right: RemoveFirst<T['right']>
}