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

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']>
}