Skip to content

Instantly share code, notes, and snippets.

@ricokahler
Created June 11, 2021 21:50
Show Gist options
  • Save ricokahler/f23314fc811126b100bdc66103e36306 to your computer and use it in GitHub Desktop.
Save ricokahler/f23314fc811126b100bdc66103e36306 to your computer and use it in GitHub Desktop.
another proof of turning completeness — 4 years later

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

// 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"
@ricokahler
Copy link
Author

ricokahler commented Jun 11, 2021

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment