Simple proof of Turing completeness for Typescript Type language
type True = true;
type False = false;
type Nand<B1, B2> = B1 extends True ? (B2 extends True ? False : True) : True;
The code above implements a NAND gate using Typescripts type language. What this means is, the compiler can evaluate the result in the editor itself without actually executing the code. For example:
let a: Nand<True, True>; // type a = False
let b: Nand<True, False>; // type b = True
You don't need to execute this code, just hover over the variables a and b in your editor, the type of the variable will be evaluated by the compiler.
Why does this prove Turing completeness?
NAND is a universal gate which is the basis of all digital computers. Which is to say any computable function can be implemented using the type language, for example to calculate the factorial of a number or solve sudoku puzzle. That does not mean it is going to practically feasible to do so... but theoretically possible.
Can we similarly implement other gates?
Yes, below are implementation of NOT and AND using the above NAND gate.
type Not<B> = Nand<B, B>;
type And<B1, B2> = Not<Nand<B1, B2>>;
Any other interesting links?
https://www.nandgame.com/
The above link teaches the fundamentals of digital computer using a game which is the inspiration for the proof.
https://github.com/eamonnboyle/sudoku-type-solver
The above link implements a sudoku solver using Typescript Type language.
Simple proof of Turing completeness for Typescript Type language
The code above implements a
NANDgate using Typescripts type language. What this means is, the compiler can evaluate the result in the editor itself without actually executing the code. For example:You don't need to execute this code, just hover over the variables
aandbin your editor, the type of the variable will be evaluated by the compiler.Why does this prove Turing completeness?
NANDis a universal gate which is the basis of all digital computers. Which is to say any computable function can be implemented using the type language, for example to calculate the factorial of a number or solve sudoku puzzle. That does not mean it is going to practically feasible to do so... but theoretically possible.Can we similarly implement other gates?
Yes, below are implementation of
NOTandANDusing the aboveNANDgate.Any other interesting links?
https://www.nandgame.com/
The above link teaches the fundamentals of digital computer using a game which is the inspiration for the proof.
https://github.com/eamonnboyle/sudoku-type-solver
The above link implements a sudoku solver using Typescript Type language.