another proof of turning completeness — 4 years later

README.md

there's a somewhat older github issue in the typescript repo that made the observation that typescript was turning complete

linked was also a proof via implement a turing machine within the typesystem.

that proof no longer works, and with the addition of template literal types, there comes a much more straightforward way to do this. that's what this is — a proof that typescript's type system is turning complete, 4 years later

see here for a typescript playground link

busy-beaver-3-state.ts

// 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"

apparently i can't type "turing" lol

honestly the most interesting thing about this is probably how readable it is. it doesn’t take much imagination to make this work nowadays lol