More than 1 year has passed since last update.

型Advent Calendar 2019

TypeScriptはgradual typingシステムか

Last updated at 2022-03-08Posted at 2019-12-15

概要

TypeScriptは，動的型付けシステムであるJavaScriptに静的型システムによる検査を部分的に導入できるプログラミング言語であり，gradual typing （漸進的型付け）システムであるとされることがあります．Siekらは，動的型付けと静的型付けの融合を図るシステム全般が無闇にgradual typingを名乗ることを疑問視して，gradual typingシステムが満たすべき基準を提案しました．本稿では，この基準に照らしてTypeScriptがgradual typingの条件を満たしていないことを指摘します．特に，ランタイムの型チェックを行わないというTypeScriptのデザインが，gradual typingの意味での健全性を明らかに阻害しています．

1 背景

ソフトウェア開発が大規模化する状況において，コード品質の担保や開発速度の維持は重要な課題です．静的型付けの手法はこの課題に対処するための手段として広く用いられています．Web開発においては長い間JavaScriptが主要な開発言語として用いられてきましたが，近年の大規模化するWeb開発においては静的手法の欠如が問題となりました．

1.1 TypeScript

TypeScript¹は，Microsoftにより開発されているプログラミング言語です．TypeScriptはJavaScriptを拡張した構文を持ち，既存の構文に型アノテーションを追加することができます．また，それを補助するものとして，型エイリアスや関数オーバーロードを宣言する機能も用意されています．TypeScriptコンパイラは型アノテーション及び型推論機構²を基にTypeScriptプログラムを静的に検査し，プログラムのある種の誤りを検出する機能を持ちます．

TypeScriptの最も大きな特徴のひとつはany型の存在です．ある値がany型を持つ場合，その値に対する一切の操作はTypeScriptコンパイラによるチェックの対象となりません．特に，潜在的に危険な操作であってもany型を用いることで型検査を成功させることができます．これは時として，型情報と矛盾する挙動を実行時に引き起こしたり，実行時エラーという結果に繋がったります．

TypeScriptにany型が存在する理由は，型をオプショナルなものとするためです．実際，TypeScriptのGitHubリポジトリには“TypeScript adds optional types to JavaScript”（強調は筆者）³と記載されています．ここで，オプショナルというのは，プログラム全体を型検査しなくてもよいということを指していると考えられます．実際，TypeScriptではあらゆる型アノテーションが省略可能です．TypeScriptコンパイラは原則として，型アノテーションが提供されているところや，型アノテーションが無くても型を推論可能なところのみを型検査の対象とします．

このような「型アノテーションが存在するところのみを型検査の対象とする」という挙動を，静的型付け―あるいは静的型システム―の枠組みで表現するための道具がany型です．TypeScriptコンパイラは型アノテーションが存在しない変数をany型として扱うことで，その変数が関わる部分の型検査を実質的に無効化します．そもそも，TypeScriptコンパイラの型推論においては，変数の型は原則として宣言時に決定されます．これはHindley-Milner型推論⁴のような，変数の使われ方から型を推論できる方法とは大きく異なる特徴です．関数の引数も例外ではなく，一部の場合（contextual typeにより型が推論可能な場合など）を除いて，引数の型は明示的に宣言しなければいけません（ちなみに，多相関数も明示的に型引数を宣言しなければいけません）．それにも関わらず変数や引数の型アノテーションが省略された場合，TypeScriptコンパイラはその変数の型の情報を得られない状態となります．TypeScriptはこのような場合にその変数の型をanyとすることで解決するというデザインを採用しています．それ以外にも，変数の型が推論できないさまざまな場面においてany型が当てはめられます．

この特徴により，TypeScriptはJavaScriptからの移行を支援しています．そもそも，ただのJavaScriptプログラムは，型アノテーションが完全に省略されたTypeScriptとみなすことができます．この状態から徐々に型アノテーションを追加することによって，TypeScriptによる型検査が行われる部分を段階的に増やすことが可能です．この段階において，TypeScriptプログラムは型検査が行われる部分と行われない部分が混在している状態となります．

なお，any型は型検査を無効化するため，型が不明な変数が自動的にany型となるのは安全性の観点からは望ましくありません．TypeScriptコンパイラは安全性が重要なユースケースに対応するコンパイラオプション--noImplicitAnyを備えています．このオプションを利用する場合，変数の型が不明な場合にはany型となるのではなくコンパイルエラーが発生します．JavaScriptからTypeScriptに移行途中であるといったシチュエーションは除くとしても，筆者はこのコンパイラオプションを有効にしてTypeScriptを利用することを強く推奨しています⁵．

1.2 Gradual Typing

Gradual typing （漸近的型付け）⁶は，SiekとTahaが2006年に提案した，静的型付けと動的型付けを融合させる手法のひとつです．静的型付けと動的型付けは異なる利点と欠点を持つものとして共存してきたものであり，両方の手法を取り入れる方法も古くから模索されてきました．Gradual Typingではこれら2つの方式をひとつのプログラムの中に共存させることができます．特に，プログラマがアノテーションを用いて，プログラムのどこに静的な検査を適用できるという特徴を持つようなシステムがGradual Typingと呼ばれます．当該論文では，特に関数型言語に対してGradual Typingの要件を満たす型システムを提案しています．

Siek & Tahaの型システムでは，通常の型に加えて $?$ 型が導入されています．$?$型が与えられた変数は静的なチェックが行われません．その点で，これは静的型検査の対象としないというアノテーションを表す型と見なすことができるものであり，TypeScriptのany型に相当します．

TypeScriptもまた静的型付けと動的型付けを融合させるという特徴を持つことから，gradual typingシステムであると見なされることがあります⁷．

2 Siek & Taha の体系の型安全性

Gradual Typingにおいては，プログラムの（型の側面での）正しさを静的に保証することは当然ながらできません．$?$型によって静的な検査を無効化した隙に誤りが入りこむかもしれないからです．Siek & Tahaの論文の序盤から例を引用します．

((λ (x) (succ x)) #t)

これは彼らが提案した計算体系 $\lambda^{?}_{\rightarrow}$ の式ですが，TypeScriptに直すと以下に相当します．

((x: any) => succ(x))(true)

ただし，succは予め定義されている関数です．

const succ = (x: number) => x + 1;

上の式は，実行するとtrueというboolean型の値がsucc関数に渡されます．succはnumber型の引数を渡すべきですから，これは誤ったプログラムということになります⁸．

ただし，上の式は型システムによる静的検査をくぐり抜けます．これは，xという$?$型（any型）を持つ変数を経由しているからです．変数xに値が入った時点で，型システム上ではその値が本来何型であるかという情報は消えています．また，$?$型はどのような型としても使用できますから，number型を受け取る関数succにxを渡しても問題ありません．

Siek & Taha の体系$\lambda^{?}_{\rightarrow}$においては上記のように誤ったプログラムはどのような結果になるのでしょうか．実はこの体系ではランタイムに誤りを検知します．これは，キャストの情報を値に保存するセマンティクスによって実現されます．

Gradual typingにおいては$?$型の存在が注目されますが，それに加えてランタイムのチェックを合わせてひとつの理論であるということは強調するに値します⁹．

この体系では，プログラムの意味は別の体系$\lambda^{\left<\tau\right>}_{\rightarrow}$のプログラムへの変換を通して理解されます．上記のプログラムは以下のように変換されます．

((λ (x : ?) (succ <number>x)) <?>#t)

元々のプログラムとの違いは，<number>xや<?>のように値の前に型が書かれている部分がある点です．このような式はキャスト式と呼ばれます．このプログラムでは，「boolean型の値を$?$型として使う」や「$?$型の値をnumber型として使う」といった操作がキャスト式によって明示的に表現されています．

上のプログラムを実行すると，変数xに<?>#tが入るので，<number>xは<number><?>#tという値になります．#tがboolean型であることに留意すると，ここでboolean型からnumber型へのキャストが発生していることが明らかになります．これは誤りなので，ここでランタイムエラー（CastError）が発生します．

以上の説明は当該論文に沿って説明したものであり、人によっては難解に感じられるかもしれません。身も蓋もないことを言ってしまえば、この体系では全ての場所に型アノテーションに従ったランタイム型チェックを入れることで誤りを検知しエラーを発生させるということになります。ただし、型情報を積極的に活かしている点は注目に値します。。例えば、「succ関数はnumber型の値を受け取る」ということに対するランタイムの型チェックは、succ関数の中ではなくsucc関数を呼び出す側に配置されます。これにより，なるべく早いタイミングで型の誤りをキャッチできるようになっています。また、型情報を活用することで、静的なチェックが済んでいるところはランタイムのチェックが省略できるようになっています。

当該論文では，彼らの体系の“型安全性“の証明が与えられています．$?$型の存在により型の誤りがランタイムに発生することは避けられませんが，それは全て上述のCastErrorとしてキャッチされます．ここでの型安全性は，上述のランタイム機構をすり抜ける型の誤りが発生しないという意味で用いられています．実際，上記でインフォーマルに説明した通り，型アノテーションに反する値がランタイムに発生することはありません．

3 Criteria for Gradual Typing

前述の論文以降gradual typingという言葉は知名度を増しましたが，その結果としてgradual typingという言葉が何を指しているのか曖昧になり，静的型付けと動的型付けを融合させる試みが無秩序にgradual typingを名乗るという問題がありました．Siekら¹⁰の2015年の論文はこの問題を指摘し，gradual typingを名乗るシステムの条件 (criteria) を整理しました．

Gradual typingシステムが満たすべき条件は以下の通りです（論文のTheorem 1から5）．2006年のオリジナルの体系はこれらの条件を全て満たすことが示されています．以下の解説は非常にインフォーマルです．

静的型付けの体系を内包する．すなわち，全ての型がアノテートされている（$?$型を用いない）プログラムは，ただの静的型付けシステムと同じ挙動をする（静的検査の結果も，実行結果も同じである）．
動的型付けの体系を内包する．すなわち，型アノテーションが無い（全ての型が$?$である）プログラムはただの動的型付けシステムと同じ挙動をする．また，任意の式の型が?である．
健全性．前節で述べたように，ランタイムにキャッチできない型の誤りは発生しない．
Blame-Subtyping Theorem．$T_1 <: T_2$（$T_1$が$T_2$の部分型）ならば，$T_1$から$T_2$へのキャストはランタイム型エラーの原因とならない．
Gradual Guarantee．すなわち，静的型検査に成功するプログラムから型アノテーションを減らしても静的型検査は成功し，型も（アノテーションが減る以外は）変わらない．また，プログラムから型アノテーションを減らしても動作が変わらない（ただし，キャッチできるランタイム型エラーが減る可能性はある）．

なお，4に出てくる部分型関係は以下のように定義されています（前述の論文¹⁰から引用）．この論文では今まで$?$型と呼んでいたものが$*$型となっています．なお，$G$というのは基本型（booleanなど）または$* \to *$です．

この定義からは$number <: *$や$* \to number <: number \to number$，また$* \to number <: *$などが成り立ちます．一方，$number \to * <: *$のようなものは成り立ちません．

部分型関係における$*$の扱いは注目に値します．特に，$* <: T$となる$T$は$*$だけです．$*$は静的解析において型エラーの原因にはなりませんが，ランタイム型エラーの原因となります，それゆえ，（特に上述の定理4の観点からは）他の型の部分型とはなれないのです．

4 TypeScriptの型システムはgradual typingシステムか

前節では，Siekらによる，Gradual typingシステムが満たすべき基準を述べました．では，TypeScriptの型システムはこの基準を満たしているのでしょうか．

4.1 TypeScriptの型システム

TypeScriptの型システムは，完全に静的なシチュエーションにおいても健全性を持たないことが広く知られています¹¹．しかし，本稿においてはこのような性質は無視し，TypeScriptがgradual typingシステムであるという主張の根幹たるany型にのみ注目します．その他の部分は一般的な静的型付きシステムと見なすこととします．

静的型検査の側面において，TypeScriptのany型はSiek & Tahaのgradual typing型システムにおける$?$型と同じ特徴を持ちます．すなわち，any型の値は他の任意の型の値が必要な場面において使用可能です．また，any型が求められる場面においても任意の型の値をany型として使用することができます．

一方で，TypeScriptのランタイムの挙動は$\lambda^{?}_{\rightarrow}$とは大きく異なります．具体的には，ランタイムの型チェックが行われません．そもそも，TypeScriptには型の情報によってランタイムの挙動が変化しないという大原則があるため，2節で説明したような型情報ベースのランタイム型チェックは趣旨に沿いません．このようなデザインを取っている理由として，型システムによるランタイムのオーバーヘッドを避けることが第一に挙げられます．また，型によるランタイムの挙動への影響を排除することで，JavaScriptユーザーから見てTypeScriptのコンパイル処理の透明性を向上するという目的があると推測されます．

上記の理由から，any型の存在に起因する型のミスマッチは，$\lambda^{?}_{\rightarrow}$におけるCastError（ランタイム型エラー）のような形でキャッチされるのではなく，別の予期せぬ形で現れることとなります．これは，TypeScriptの型システムでは，gradual typingの意味での健全性が失われていることを意味ます．

以降でもランタイム型エラーという語を用いますが，これはgradual typingシステムによるランタイムのチェックによって検出されるものを指すことに注意してください．実際のTypeScriptでは，型のミスマッチは呼びだそうとしたメソッドが存在しないことによる実行時エラーや，undefinedやnullに対するプロパティアクセスしたことによる実行時エラーなど，その結果はさまざまな形で現れます．本稿では，これらは前述のランタイム型エラーとは区別し，予期せぬ結果と呼んでいます．ランタイム型エラーはプログラムの動的な部分のチェックが正しく行われた結果として現れるのに対し，予期せぬ結果は，システムの健全性が失われた結果として現れるものです．

4.2 TypeScriptとCriteria for Gradual Typing

では，TypeScriptの型システムの性質をSiekらのcriteria for gradual typingに照らし合わせてみます．

1（静的型付けの体系を内包する）と2（動的型付けの体系を内包する）については成り立ちます．というよりも，1と2は変なセマンティクスを持つ体系を除外するための条件であると考えられるので，これらの条件は今回の設定ではあまり意味を持ちません．1に関してはTypeScriptと比較するための静的なシステムが必要ですが，それはanyを取り除いたTypeScriptそのものです．

2については比較対象の動的システムはJavaScriptとなりますが，上述の性質から2が成り立つことは明らかです．ただし，この条件をTypeScriptに当てはめる際には注意すべき点があります．本来のTypeScriptでは「任意の式の型がany型である」は満たされません．例えば次のプログラムにおいて変数vはnumber型です．

const x: any = 123;
const y: any = 456;
const v = x * y;

しかしながら，これは*演算子の挙動によるものです．Siekらが本来対象としているのが関数型言語であることを鑑みると，*のような計算も全て関数としてみなすのが適切です．Siekらの論文にも，2の条件については組みこみ定数や関数も全て$*$型として見なすものと定義されています．実際，このことをより忠実に反映した以下のTypeScriptプログラムでは変数vの型はanyとなります．

const mul: any = (x: any, y: any) => x * y;
const x: any = 123;
const y: any = 456;
const v = mul(x, y);

3つ目の条件である健全性については，すでに議論した通り，明らかに満たされません．そもそもランタイムのチェックがまったく行われないからです．

4についても状況設定から議論する必要があります．部分型からのキャストはランタイム型エラーの原因にならないという条件ですが，そもそも全くランタイムの型チェックが行われない設定では意味のある主張ではありません．一方で，その他の予期せぬ結果もここでのエラーに含めることも考えられます¹²．ただし，その場合は，健全性が失われていることから反例を作るのは簡単です．

最後の条件，gradual guaranteeについては，TypeScriptの言葉で言い換えれば，型アノテーションを減らすというのは型註釈を何らかの型からanyに変えることを指します．ランタイムの動作については，前述の性質から型註釈がanyに変わってもランタイムの動作が変わらないことは自明です．一方で，静的型検査については自明ではありません．

--noImplicitAnyコンパイラオプションが有効の状況では，以下のプログラムが反例となります．変数keyの型註釈をany型に変更すると，obj[key]という式がコンパイルエラーを発生させます．これは，any型の式をプロパティアクセスのキーに用いることによってobj[key]という式の型がanyとなることを警告するものです．

const key: "foo" = "foo";
const obj = { foo: 123 };

obj[key];

ただし，筆者は--noImplicitAnyによるコンパイルエラーがこの議論において本質的なものであるかどうか判断しかねています．これを本質的でないとみなす立場からは，keyの型がanyである以上obj[key]の型がanyとなることは当然であり，--noImplicitAnyによるチェックは議論に含めるべきでないと言えます．また，条件2において触れたのと同様に，プロパティアクセスという特有の構造を関数に抽象化することによってもやはりこのエラーは消すことができます．

一方で，過度に抽象化するのはTypeScriptについて議論する意義そのものを薄めるため避けるべきであり，これをgradual guaranteeから逸脱する挙動として受け入れるべきとする意見も考えられます．

本稿ではこの議論に強い興味があるわけではないため，ここでは問題を提起するのみに留めます．

以上の5条件について議論した結果において，TypeScriptのanyが（gradual typingの意味での）健全性を失っていることがTypeScriptの顕著な特徴として現れています．ランタイムの型チェックを行わないことはTypeScriptの根本的な言語デザインであり，その点においてgradual typingとは乖離していることが分かりました．

5 Safe TypeScriptにおける対応

前節では，TypeScriptが（gradual typingの意味においても）健全性を持たないことでgradual typingの基準を満たしていないことを指摘しました．この問題に対応するアイデアのひとつがSafe TypeScript¹³です¹⁴．これは，健全性を保ったバージョンのTypeScriptとしてMicrosoft Researchにより開発されたものです．ただし，あくまで研究レベルの成果であり，直ちにプロダクション開発に利用可能なものではありません．

Safe TypeScriptが健全性を得るために行なった変更は大きく分けると2つあります．一つは型システムへの変更により静的検査における健全性を確保することであり，もう一つはランタイム型チェックの導入によりgradual typingの意味での健全性を確保することです．実際の論文では，ランタイム型チェックのオーバーヘッドを削減するための工夫が述べられており，それらによってランタイム型チェックのオーバーヘッドが15%程度に抑えられたことが報告されています．

ランタイム型チェックの一例が下の図に現れています（当該論文¹³から引用）．関数fの返り値であるx.fが本当にアノテーション通りのnumber型であるかどうかランタイムにチェックするためのRT.checkという呼び出しが追加されていることが分かります．

Figure 1: Architecture of Safe TypeScript

Safe TypeScriptは明確にgradual type systemを名乗っています．実際，論文で主張されている通りSafe TypeScriptはgradual typingの意味での健全性を備えているようです．Siekらの条件に照らし合わせたときに4番目と5番目が満たされるかどうかは直ちに明らかではなく，本稿では残念ながらそこには触れません．

6 結論

本稿では，Siekらの基準に照らしてTypeScriptがgradual typingの条件を満たしていないことを指摘しました．特に，TypeScriptはランタイムの型チェックを全く行わないという言語デザインを採用しているため，gradual typingの意味での健全性を明らかに満たしていません．その一つの理由として，ランタイムのオーバーヘッドの存在が考えられます．実際，健全性を満たすバージョンとして提案されたSafe TypeScriptでは，オーバーヘッドを減らす様々な工夫を行ってもなお，15%のオーバーヘッドが存在しています．

本稿は，TypeScriptがgradual typingの基準を満たさないことを以てTypeScriptを批判しようとするものではありません．筆者はTypeScriptの言語デザインはそれがプロダクションレベルで使われる言語として有るために必要なものだと考えています．それよりも，TypeScriptという題材を通じて読者にgradual typingを理解させることを目的としています．読者がgradual typingをより深く正確に理解し，TypeScriptやgradual typingに対する議論の糧とすることを期待します．

https://www.typescriptlang.org/ ↩
cf. TypeScriptの型推論詳説 - Qiita ↩
https://github.com/microsoft/TypeScript . 2019年12月4日閲覧． ↩
Robin Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences. 17 (3): 348–374, 1978. ↩
cf. 敗北者のTypeScript - Qiita ↩
Jeremy Siek, Walid Taha. Gradual Typing for Functional Languages. In Scheme and Functional Programming 2006: pages 81–92. ↩
TypeScriptが公式にgradual typingを名乗っていた時期があったと記憶していますが，資料を見つけることができませんでした．これに関する情報をお持ちの方はご提供いただけると幸いです． ↩
なお，TypeScriptでは実行時エラーなどではなく2という結果になりますが，それは本質的なことではなりません．一般には誤ったプログラムは意図しない挙動や実行時エラーの可能性があります． ↩
yigarashi. 漸進的型付けの未来を考える． In yigarashiのブログ, 2017. ↩
Jeremy Siek, Michael Vitousek, Matteo Cimini, John Boyland. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages, SNAPL (LIPIcs). 32: pages 274–293, 2015. ↩ ↩²
kgtkr. TypeScriptのunsafeな操作まとめ. In Qiita, 2018. ↩
Siekらは4番目の条件をblameに付与されたラベルを用いて定義していますから，ランタイム型エラー以外に対してその原因が何かを考えるのは非常にインフォーマルな議論にならざるを得ませんが． ↩
Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris. Safe & Efficient Gradual Typing for TypeScript. In POPL 2015, pages 167-180, 2015. ↩ ↩²
ただし，論文の発表順はSiekらのcriteria for gradual typingよりもSafe TypeScriptの方が先です． ↩

135

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up