TypeScriptの型システム(型計算)は、チューリング完全であると言われています。つまり、誤解を恐れずに言えば、計算機でできるすべての計算はTypeScriptの型システムでもできるというわけです！ これは驚くべきことです。「TypeScriptでもできる」ではなくて「TypeScriptの『型システムでも』できる」なのです。要するに、型システム単体で計算機の代わりになるというのです。 でも、それって本当なのでしょうか。パソコンという身近な計算機一つをとってもいろいろなことができます。四則演算はもちろん、ゲームプログラミングから型推論まで、本当にたくさんのことができます。 そして、TypeScriptの型システムを使えばそれらすべてができるというのです。にわかには信じられません。 型システムで四則演算ができるのでしょうか？ 型システムでゲームが作れるのでしょうか？ ……もしかして、型システムで型システムを実装できるのでしょうか？ というか、そもそも「計算機でできる計算はTypeScriptの型システムでぜんぶできる」だなんて言う人は、何を根拠にそんなことを言うのでしょうか。 というか、もっと言えば、ある計算を取り上げて「この計算は計算機でできる/できない」だなんて言うとき、それは何を意味しているのでしょうか。 気になるのは理論的な側面だけではありません。 「TypeScriptの型システムはチューリング完全である」という事実は、TypeScriptを使う開発者にどのような利点と欠点をもたらすのでしょうか。 チューリング完全であること、つまり「計算機代わりになるという性質」には何のデメリットもないように見えます。でも、本当に何の心配もないのでしょうか。 このセッションでは、「TypeScriptの型システムはチューリング完全である」という主張を証明しながら、型理論やチューリング完全性、そしてクワイン(自分自身を出力するプログラム)に関する計算理論をふかぼっていきます。 そして、型システムがチューリング完全性を帯びて「しまう」理由、帯びることによる不都合やその回避可能性といった、決まった答えのない問いについても考察してみます。 TypeScriptと一緒に、計算の不思議でおもしろい世界へと飛び込みましょう！