「型システム入門」の先へ：TypeScriptの型システムのいくつかの側面

この記事は TypeScript Advent Calendar 2023 の8日目の記事です。言語実装勢にも役立つ内容を含んでいるかもしれないので、 言語実装 Advent Calendar 2023 にも登録しています。

TypeScriptで型システムに興味を持った人が「型システム入門」を読んだという話を時々聞きます。「型システム入門」は、Types and Programming Languages (TAPL) という本の邦訳で、型システムに興味を持った人が読むのは自然なことです。

ですが、この本の原著は2002年出版で、最近の話題がカバーされていなかったり、邦題に「入門」とあるように発展的な話題は扱っていなかったりします。一応続編的な感じのAdvanced Topics in Types and Programming Languages (ATTAPL) という本はありますが、これも2004年なので最近の話題はカバーされていません。

そして、TypeScriptの型システムは最近の型の理論／技術をちょいちょい使っています。

そういうわけで、私としては、TypeScriptで型システムに興味を持った人が辿り着くのが「型システム入門」止まりで本当に良いのか、という気持ちがあります。「型システム入門」の先を見たくはありませんか？

残念ながら私は型理論の専門家ではなく、高度な型システムの理論的な説明はとても書けません。なので、この記事ではTypeScriptの型システムのいくつかの側面を紹介し、文献へのポインターを提示することにします。

なお、私はTypeScriptの実装は読んでいません。あくまでドキュメントや挙動を見て判断しています。

漸進的型付け：gradual typing

TypeScriptの型システムの特徴として真っ先に挙げられるのが「何でも入る型」 any 型の存在です。any 型の変数にはどんな型の値でも代入することができ、any 型の値はどんな型の変数にも代入できます。「型システム入門」で部分型付けを学んだあなたは、any 型は「全ての型の部分型であり、それと同時に全ての型の上位型である」と思うかもしれません。

しかし、その状況で部分型付けの規則を使うと、任意の型 T と U に対して T <: any <: U かつ U <: any <: T が成り立つことになり、任意の型 T と U に互換性があるという結論が得られてしまいます。型システムが縮退してしまうのです。これでは型なしの言語と同じで、コンパイラーは何に対して型エラーを出せばいいのかわかりません。

2006年に提案されたgradual typingは、型システムを縮退させることなく、「任意の型と適合する型」any の導入を可能にします。詳しくは以下の論文を参照してください。

  • J. G. Siek and W. Taha. 2006. Gradual Typing for Functional Languages, In Proceedings of Scheme and Functional Programming Workshop. ACM, 81–92

ブログ記事もあります。

元々のgradual typingは部分型や多相型を持たないシステムに対してでしたが、現実のTypeScriptには部分型も多相型もあります。gradual typingをそのようなシステムに拡張する研究は探せば出てくると思うので、各自で探してください（私は型システムの専門家ではないので……）。

なお、原論文では実行時検査を行うことによって「健全性」を主張しています。一方でTypeScriptは実行時検査を行わないので、gradual typingではないのでは、という議論もあります。

まあこの記事はTypeScriptをダシにして型システムの話題を紹介する記事なので、TypeScript自体が何なのかはそこまで気にしません。

言語実装勢向け：最近公開された「自作言語を10年やってわかったこと」みたいな記事に「gradual typingはやめとけ」みたいな話がありました。gradual typingは新規の言語には向かない機能なのかもしれません。

局所型推論と双方向型付け：local type inference / bidirectional typing

TypeScriptのデフォルトでは、型がわからない変数には any 型がつきます。例えば、以下の関数の引数 a には型注釈が与えられていないので、TypeScriptは any 型を割り当てます。

function foo(a) {
    return a.someMethod();
}

一方、MLやHaskellには強力な型推論（型再構築）があるので、関数の引数の型注釈を与えなくてもコンパイラーが引数の使われ方から型を判断してくれます。TypeScriptでも型推論できないのかというと、MLやHaskellとは違い部分型やら何やらがあるので、そこまで強力な型推論はできません。

しかし、引数の使われ方から型を推論できないからといって、全ての関数の引数に型注釈を書かせる（さもなければ any になる）というのはあまりにも不便です。次のコードを考えます。

function addEventListener(callback: (e: Event) => void);

addEventListener(e => { console.log(e.someData); });

addEventListener 関数の引数に与える無名関数の引数 e の型は、人間が見れば Event 型であることがわかるでしょう。変数の使われ方から型を推論することができなくても、関数の書かれた文脈から型を推論できる場合があるのです。賢いコンパイラーなら、上記のコードの e に対して any ではなく Event 型を割り当てることができて良いはずです。

局所型推論 (local type inference) は、「文脈」を活用することにより一部の型注釈の省略を可能にします。局所型推論の論文を紹介しておきます（「型システム入門」にも言及がありますね）。

この論文では、無名関数の引数の型を推論する話のほかに、型引数を推論する話も扱っています。

この論文は部分型と多相性を持つシステムでの話ですが、局所型推論は、その後、双方向型付け (bidirectional typing) に発展していくようです。双方向型付けは強力で、部分型や多相型だけでなく、依存型にも適用できるようです。双方向型付けについての最近のサーベイを挙げておきます：

双方向型付けについての日本語の記事も紹介しておきます：

flow-sensitive typing (occurrence typing)

普通の型システムでは、一つの変数の型はそのスコープ内で変化しません。次のコードを考えてみます。

function foo(x: string | number) {
    if (typeof x === "string") {
        return parseInt(x);
    } else {
        return x * x;
    }
}

x の型は string | number で、parseInt は string しか受け付けないので、上記のコードはエラーになる……ということはなく、TypeScriptは上記のコードを受理します。これは、TypeScriptが typeof x === "string" という式と条件文を見て、then部分では x が string 型だと判断したからです。このように変数のテストによって型の詳細化を起こすのをflow-sensitive typingとかoccurrence typingとか呼びます。

このトピックについて私はマジで詳しくないのでアレなんですが、軽く調べた感じではTyped Scheme（今のTyped Racket）が先駆者であるようです：

  • Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The design and implementation of typed scheme. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’08). Association for Computing Machinery, New York, NY, USA, 395–406. https://doi.org/10.1145/1328438.1328486

関連

TypeScriptの型検査っぽいものを作る記事も紹介しておきます：

この記事でもnegation typesを紹介するべきだったかもしれません（よくわかってない）。

最後に

私のような素人ではなくて型理論ガチ勢が書いた「型システム入門の先」みたいな本か記事が読みたいです。誰か書いてください。

このエントリーをはてなブックマークに追加