Location via proxy:   [ UP ]  
[Report a bug]   [Manage cookies]                

TypeScriptは型安全じゃないからすばらしい

「TypeScriptではじめる型システム」という記事をn月刊ラムダノートに寄稿しました。

どんな内容？

TypeScriptの極小サブセットに対する型検査器を書き、それを通して型システムを体感してみよう、という内容です。

詳しく言うと、boolean型とnumber型と関数型しかないTypeScriptサブセット言語がターゲットです。 型検査器の実装言語にもTypeScript（処理系はDeno）を使います。 TypeScriptづくしの一品です。

わかる人向けに言うと、「型システム入門」という本（通称TAPL）の単純型付きラムダ計算に相当する内容をTypeScriptで説明してみた、ただし定理や証明はすべて省いた、という感じです。

なぜ書いた？

きっかけがいくつかありました。

TypeScript界隈でTAPLが読まれているらしいと聞いた

もともと、型システムを実務プログラマ向けに説明する記事を書いてみたいという気持ちはずっとありました。 TAPLは情報科学専攻の大学院生向けの教科書なのですが、型システムというキャッチーな内容から、実務プログラマにも注目されています。 しかしTAPLは、あまり実務で見かけないMLという言語で説明されている上、定理と証明が紙面の半分くらいを占めているので、「途中で脱落した」「型システム入門入門が欲しい」という話をよく聞いていました。

TAPLを翻訳したのは12年も前のことですが、今年になって急に、日本のTypeScript界隈でTAPLを読んでいる人たちが結構いるらしいと小耳にはさみました。 それも複数の経路で同時多発的に。 そのうちのひとつでは、TAPLの訳者として声をかけていただき、トークさせてもらいました。

これで、「いまこそ記事を書くべきなのでは？」という気分が高まりました。

TypeScriptの裏側を調べてみたかった

もうひとつの動機としては、TypeScriptの設計方針や型検査器の実装を少し真面目に理解してみたいと思ったことです。 私はTypeProfというRubyの型解析器を開発してます。

github.com

TypeProfを作るうえで、TypeScriptはいろいろ参考にしてます。 ただ、TypeScriptのユーザとしての体験は多少知っているつもりですが、裏側を真面目に見たことはなかったので、ここらで少しだけきちんと調べておきたいと思っていたのでした。 この執筆は、そのきっかけにもなりました。

TypeScriptは型安全じゃない？

そうして調べているうちにわかったのですが、TypeScriptはとてもいい意味で「雑」に作られているということがわかりました。 これは、漸進的型付けがどうこうという話ではなく、もっと全体的な設計・実装方針の話です。

TypeScriptが見逃すエラー

典型的な例としては、次のような未初期化変数の参照をするプログラムが型エラーになりません。

型検査器がこのような見逃しをする場合、型安全性があるとは言わないのがふつうだと思います。 これはTDZ（Temporal Dead Zone）と呼ばれるJavaScriptの仕様なので、ちょっと考えてみると、JavaScriptの構文を保ったまま解決するのはむずかしそうです。 実際、TypeScriptにissueがあがっていますが、「めったに出てこないケースなので気にすんな」ということでWontfixとなってました。

他にも、「全然関係ない変数宣言を削除すると、出るべきエラーが消えてしまう」という、かなり理解不能な挙動をする例も作れてしまいました。

この挙動の私の理解ですが、TypeScriptの型検査器はヒューリスティックに再帰を打ち切るところがたくさんあって、そのせいだと思います。つまりこの例は、ジェネリック型の展開打ち切りの閾値ぎりぎりのところに型エラーがあって、8行目の型判定を先にやっておくと判定結果がメモ化されることで探索範囲がぎりぎり型エラーに届くけど、8行目がないと型エラーまでの探索が深くなりすぎて打ち切られる、みたいな感じなのかなと思ってます。

ちなみに、TypeScriptが本当に型安全でないかは、型安全の定義によります。JavaScriptにトランスパイルされるので、未定義動作に陥ることは原理的にないから、「TypeScriptは何もしなくても型安全だ」という主張もふつうにありえます。このへんは記事のコラムにいろいろ書いたので参照ください。

それでもTypeScriptはよいもの

「雑」「型安全じゃない」というと、TypeScriptを悪く言っていると思われるかも知れませんが、まったく逆です。

現実問題として、TypeScriptが便利であることに異論を挟む人は少ないと思います。 JavaScriptは控えめに言っても（動的型付け云々以前に）いろいろと厳しい言語だと思うのですが、TypeScriptはJavaScriptのハンデを負ってなお便利なので、文句なくすごいです。

型システムに詳しい人は型安全性を気にしがちなのですが、TypeScriptは「別に全部の型エラーを検出できなくてもよい（型安全じゃなくてよい）」という思い切った割り切りをしています。 それでいて、「現実的によくあるバグは大体検出できて便利」という絶妙なバランスを達成しています。

ちなみに、ちょうどkmizuさんがほぼ同じようなことを言ってました。

TypeScriptの設計者の言葉

Anders Hejlsberg自身が、次のように言っています。

If you can't achieve perfection then you don't even try to go there and that means you cut out a whole bunch of possible things that you could do that you might not be able to prove soundness for, but we don't have that restriction and that actually makes our work very interesting because we can go in places where people typically don't go.

雑な意訳：型の研究者は型安全性が証明できそうにないことと試そうともしないので、実はいろいろできることを切り捨ててしまっている。TypeScriptにはそういう制約がない。そのおかげでわれわれは、他の型研究者がふつうは行かない領域に踏み込めるので、とても面白い仕事ができている。

www.youtube.com

これ、型の研究者には結構辛辣ですね。

個人的には、「ぜんぜん型安全じゃなくても便利な型解析器」は実際に存在できるんだというのが確信できてよかったです。 TypeProfもそういうところを目指していて、実現できるのか自分でも半信半疑でやっているのですが、達成した実例があるというのは心強く感じました。 TypeProfがそのクオリティとバランスを目指したいものです。

記事について雑多なこと

パーサはどうした

TypeScriptサブセットの型検査器を作るためにはパーサが必要だったのですが、その書き方を解説していると日が暮れるので、あらかじめ用意しておきました。

https://github.com/LambdaNote/support-ts-tapl/blob/main/utils.ts

eslintで使われているtypescript-estreeをラップする感じで作ってます。

TypeScriptプロジェクトのよい書き方がわからなかったので、とりあえずDeno専用になってます。 TypeScriptに詳しい人がみたら変な感じになってそうなので、適当にPRくれるとうれしいです。

Rubyじゃないのはなぜ

Rubyの型の開発に参加している立場でありながら、Ruby + RBSを記事の題材にしなかったのは、上に書いた動機のとおりなのですが、さらに技術的な理由として、Rubyでは無名関数が第一級の言語機能じゃないからです。 TAPLベースの型システムを説明したいという記事の方向性には、無名関数が必要でした。 もちろんProcはありますが、defを使わずにProcだけでプログラムを書くのはふつうのRubyじゃなさすぎるので。

続きが読みたい

単純型付きラムダ計算で終わっているので、人によっては「これで終わり？」って思うかもしれません。 basic.tsは部分型付け、型エイリアス、ジェネリクスなどを付け足していくための土台になっています。 今回の反響がよければ、それらで言語拡張するという続きを出せたらと思っています。