この記事はCAMPHOR- Advent Calendar 2017 11日目の記事です．

アブストラクト

漸進的型付けは，ひとつの言語の中で静的型付けと動的型付けをスムーズに組み合わせるための技術です．よく知られた特徴は any 型を使った静的型付けで， TypeScript や Python といったプログラミング言語には既に実装されています．しかし，理論と実際のプログラミング言語の間には大きなギャップが存在します．特に，漸進的型付けの理論で提案されているキャストを用いた動的型検査が実装されていないために，静的型付けの恩恵を十分に得られていないという問題があります．この記事では，まず漸進的型付けの理論をコード例を用いて紹介し，現状の漸進的型付き言語が抱える問題を解説します．そのあとで，漸進的型付き言語が目指すべき目標を理論的視点から論じます．それらの目標は，静的型付けを行うこと，キャストを用いた動的型検査を行うこと，動的型検査を効率よく行うこと，型情報に基づいて最適化を行うことの4段階に分類することができます．未だ実現されてないこれらの目標を論じることで，多くの人に漸進的型付けの未来を考えてもらうのが本記事の目的です．

1. はじめに

近年，漸進的型付き言語を使うプログラマーが増えています．多くの人がそんな難しい言葉は知らないと言うでしょうが，漸進的型付け（Gradual Typing）は確実にあなたの身近な技術となりつつあります．最も典型的な例は TypeScript です．TypeScript は JavaScript のスーパーセットで， JavaScript に型アノテーションの文法といった拡張を施し静的型付けを取り入れた言語です．静的型付け自体は，既存の多くのプログラミング言語に見られる機能で何も特別なことはありません． TypeScript が他の多くの言語と違うのは， any という型を使って動的型付き言語である JavaScript と連携する点です． any 型は動的に型検査される部分を表し，静的型付け時にはワイルドカードのように振舞います．型アノテーションが省略された場合，その部分は any 型として静的型付けが行われます．これにより TypeScript は静的型付き言語でありながら既存の JavaScript のコードをそのまま利用できます．例えば，次のような JavaScript のコードを TypeScript に輸入することを考えましょう．

function add(x, y){  // 型アノテーションがないので x，y は any 型と解釈する
    return x + y;
}

add(3, 5);  // 実引数の number 型と any 型を比較して型検査を通ると判断する

add は足し算をする関数です．型アノテーションが省略されているので TypeScript では any 型の値を受け取ると解釈されます． any 型はワイルドカードのように扱われるため，そこに number 型の値を渡すことは問題ありません．この JavaScript のコードは TypeScript の型検査をパスし，そのまま実行することができます！ any 型のおかげで既存の JavaScript のコードを無料で輸入することができました．さらに一度輸入に成功すれば，それらのコードを「漸進的に」進化させることが可能です． TypeScript では先ほどの関数を次のように変更できます．

function add(x: number, y){
    return x + y;
}

function add(x: number, y: number){
    return x + y;
}

型アノテーションを省略して any 型のままにしておいても，もともと動いていたコードはそのまま動き続けますが，上のように型アノテーションを少しずつ追加することで，必要なだけ静的型付けの恩恵を得ることができます． TypeScript では any 型をうまく使うことによって，既存の JavaScript コードに少しずつ型を追加したり，型のついたコードと既存の JavaScript ライブラリをスムーズに組み合わせたりということが可能です．このように，漸進的型付けとは any 型を用いて一つの言語の中で静的型付けと動的型付けをスムーズに組み合わせる手法のことを言います． その思想は多くの人に受け入れられ一定の成功を納めているように見えます．

しかし，2006年に Siek と Taha によって提案されたオリジナルの漸進的型付け *1と，実際に漸進的型付けの考え方を導入しているプログラミング言語の間には大きなギャップがあります．実際の言語がオリジナルの理論の一部のアイディアしか取り入れていないために，本来得られるはずの利益が得られていないという現状があります．ただ，ここで注意して欲しいのは，こうした視点から TypeScript や他の言語を非難するのは気が早いということです．理論に沿った漸進的型付けの実装が難しいことは知られており，今も多くの人が頭をひねっています．「理想的な漸進的型付き言語」は依然として未来の技術です．

では，その「理想的な漸進的型付き言語」が永久機関や錬金術のような絵空事かというと，そうではありません．いわゆる理論計算機科学者を中心として，目指すべきゴールと解決すべき問題が少しずつ具体的になっています．ラムダ計算などの理想化された世界を越えて，具体的な実装で結果が示されることも増えてきました．オリジナルの思想に基づいた漸進的型付けが広く使われる日が近づいているという予感があります．しかし，その予感を現実にするためには，今まで以上に多くの人の知恵と協力が必要だと感じています．

私がこの記事を通して目指していることは，より多くの人にこれから達成すべき目標を共有し，漸進的型付けの未来を考えてもらうことです．そのために，次の2章では漸進的型付けがどんなものであるかをなるべく正しく，簡単に伝えます．もちろんラムダ計算や難しい記号は使わず，コード例を使って解説します． 3章では，2章で解説した知識をもとに TypeScript と Python の現状を概観し，それらに共通する問題について解説します． 4章で漸進的型付けが達成していくべき目標をいくつかの段階に分けて示し， 5章で補足や議論をしてまとめます．

2. 漸進的型付け入門

この章では漸進的型付けの理論を解説します．ラムダ計算を使った形式的な定義を示したいところですが，それは本記事が目指す多くの人に情報を共有するという目的に反するので，多少の曖昧さを覚悟の上で TypeScript ライクなコード例と言葉だけで解説します．厳密な理論を知りたい方は脚注の論文を参照してください*2．

漸進的型付けは以下の二つの要素を組み合わせたハイブリッドな型付けであると言えます．

any 型をワイルドカードとして扱う静的型付け
キャストによる動的型検査

この時点で理解すべき重要なことは， 漸進的型付けが実行前の静的型付けと実行時の動的型検査の二つのフェーズからなるということです．早速，上に述べた二つのポイントについて詳しく見ていきましょう．今後現れるコード例では，説明のためにいくつかの仮定をおきます．まず，変数や関数の定義，関数適用，return は TypeScript と同じであるとします．型は number，string，any と，T1 -> T2 の形をした関数型のみであるとします． T1 -> T2 は T1 型の値を受け取って T2 型の値を返す関数の型です．見た目は TypeScript に似ていますが，あくまで説明のための疑似コードで， TypeScript ではないということに注意してください．

2.1. any 型をワイルドカードとして扱う静的型付け

漸進的型付けの実行前型検査は，any 型を含まないコードに対しては普通の静的型付けと同様に動作します．例えば，以下のような例における型付けの結果は直感通りのはずです．型検査を通る場合には結果の型を，型検査を通らない場合は Ill-typed! という文字列をそれぞれコメントで付記しています．

function example1(x: number) {
    return x + 1;
}
// number -> number

example1(42);
// number

example1("abc");
// Ill-typed!

一方で any 型が使われた部分は常にワイルドカードとして扱われます．以下の例において，any 型の引数 x にはどんな引数を渡しても型検査を通過します．

function example2(x: any){
    return x + 1;
}
// any -> number

example2(42);
// number

example2("abc");
// number

example2(add);  // add の型は number -> number -> number
// number

以下に示すように，any を複雑な型の一部として使うこともでき，同様にワイルドカードのように扱われます．

function example3(fun: any -> number){
    return 42;
}
// (any -> number) -> number

example3(f1)  // f1 の型は string -> number
// number

example3(f2)  // f2 の型は (string -> string) -> number
// number

漸進的型付けの実行前型検査のアイディアは実はこれだけです．「any 型をワイルドカードとして扱う」が全てで，難しいことは何もありません．

しかし，any をワイルドカードとする静的型付けは制限が弱く，それ単体では静的型付けによる保証が実行時に破られてしまいます．以下のプログラムを見てみましょう．

function example4(x: string) : string {
    return x;
}
// string -> string

var y : any = 42;
// any

example4(y);
// string

example4 は単なる恒等関数です．下の関数適用は y が any 型であることから型がつきます．しかし，型検査を通ったのだからと張り切ってプログラムを走らせると，とても悲しいことに気がつきます．一番下の関数適用をそのまま実行すると，string 型の値を要求している example4 に number 型の値 42 が渡されてしまうのです．本来，example4 の x が必ず string 型の値になることを保証するのが静的型付けの役割です．これでは，一体なんのための型付けだったのかわかりません．

それでは漸進的型付けは， any 型を使いつつ気休め程度に型検査をする技術なのでしょうか．当然ですがそれは違います．漸進的型付けにはもっと人々を楽しませる面白い仕組みが用意されています．次の節で，キャストによる動的型検査によって一般に望まれるような型付けの性質が得られることを見ます．

2.2. キャストによる動的型検査

2.1節では静的型付けのみでは不十分であるということを説明しました．この節では，その不十分さをカバーする漸進的型付けのもう一つのポイントを説明します．漸進的型付けでは，「キャスト」と呼ばれる動的型検査の仕組みをプログラムに挿入することで，実行時に追加で型検査を行ってプログラムの安全性を保証します．

まずはキャストがどんなものであるかを見ましょう．キャストは 42 : number ==> any のように，プログラムと二つの型からなる三つ組です．これは「42 を number 型から any 型にキャストする」と読みます．必ず成功するキャストには次のようなものがあります．

42 : number ==> number
42 : number ==> any
(42 : number ==> any) : any ==> number

一つ目のような同じ型へのキャストは必ず成功します．また，二つ目のような any 型へのキャストも必ず成功します．三つ目のような any を経由して同じ型へキャストする場合も必ず成功します．次に，必ず失敗するキャストには次のようなものがあります．

42 : number ==> string
x : number ==> (number -> number)
(42 : number ==> any) : any ==> string

上の二つのような any ではない全く異なる型へのキャストは必ず失敗します．三つ目のように any を経由した場合でも同様です．

漸進的型付けでは，型が等しくない部分にキャストを挿入して実行することで型エラーを検出します．まずは，先ほどの example4 について実際にキャスト挿入をしてみましょう．

function example4(x: string) : string {
    return x;
}

var y : any = 42;

example4(42);

// ********************************************
//  キャスト挿入結果
function example4(x: string) : string {
    return x;
}

var y : any = (42 : number ==> any);

example4(y : any ==> string);

y の宣言では，any 型の変数 y を number 型の値 42 に束縛しているので， 42 : number ==> any というようにキャストを挿入しています．その下の関数適用では，string 型を要求する example4 に対して any 型の引数を与えているので， y : any ==> string というキャストを挿入しています．このように，any 型が原因で型が等しくない部分にキャストを挿入していくのが「キャスト挿入」という処理です．

次に，キャストを挿入したあとのプログラムを実行してみましょう．実行のステップが進むことを ---> という記号で表すことにします．

example4(y : any ==> string)
---> example4((42 : number ==> any) : any ==> string)
---> Runtime TypeError!  // キャストが失敗して例外を送出

example4 に型の違う引数が渡る前に，安全にハンドルできる型エラーの例外を投げることができました．このように，漸進的型付けでは，キャストを挿入して実行することによって静的型付けを通り抜けてしまった型エラーを例外の形で安全に処理できます．キャストのおかげで，example4 のような関数は x が必ず string 型の値になるとわかります．

漸進的型付けにおける実行前の型付けは弱い保証しか与えませんが，キャストによる動的型検査の仕組みを組み合わせることで，通常の静的型付けと同様の保証を得られるようにしています． any をワイルドカードとみなすということと，型が一致しないところにキャストを挿入するという非常にシンプルなアイディアによって，静的型付けと動的型検査を一つの言語内で安全に組み合わせることを可能とした点が，漸進的型付けの最も面白いポイントなのです．

3. 漸進的型付けの現状

この章では，漸進的型付けの考え方が取り入れられている実際のプログラミング言語として，TypeScript と Python を概観します．特に2章で確認した実際の理論と見比べてどのような違いがあるかに注意して見ていきます．その後で，それらの言語に共通する問題を詳しく見ていくことで問題意識を共有します．

3.1. TypeScript

TypeScript（https://www.typescriptlang.org/）はJavaScript のスーパーセットで，型アノテーション等に基づいた静的型付けを行うことができます． any 型を含んでいることから，JavaScript をベースにした漸進的型付き言語とみなすこともできます． TypeScript のコンパイラ（トランスパイラ）である tsc は，入力された TypeScript のプログラムに対して静的型付けを行い，その後で型アノテーションを取り除くなどの変換をしてJavaScript のプログラムを出力します．この時，tsc はキャストのような動的型検査のための新たな仕組みを何も挿入しません． 2章で確認した理論に照らし合わせると，2.1節の静的型付けのみを行い， 2.2節のキャストによる動的型検査を行なわないということになります．つまり，2.1節の example4 で述べたような問題が TypeScript にも起こるということです．実際に tsc に example4 とそれらを利用するコードを入力すると，以下のような JavaScript コードが出力されます．

function example4(x){
    return x;
}

var y = 42;

example4(42);

これを実行すると，string 型の引数を受け取るはずの example4 に 42 が渡ってしまうことがわかります．

このような問題は any 型を使わなければ回避できます．プログラマが手元で書くコードに関しては，any 型を使わないようにするのは簡単です．問題はサードパーティーの JavaScript ライブラリを使う場合です． TypeScript には，既存の JavaScript モジュールに対する型定義ファイルを集めた DefinitelyTyped（http://definitelytyped.org/）というリポジトリが存在します．非常に多くの型定義ファイルが集まっており，かなりの数の JavaScript ライブラリを TypeScript で利用できることがわかります．しかし，それらの型定義はユーザーに提供されるインターフェースに限られ，関数内部や内部モジュールまで完全に型検査が行われるわけではありません．静的型付けを行なっていない部分で型を変える操作を行なっていれば，型定義ファイルや静的型付けの結果を他の静的型付き言語のように信じることはできません．従って，キャストのような動的型検査無しに上のような問題を根絶することは難しいと考えられます．

上に述べたような欠点はありますが，もともとは JavaScript という静的型付けのない言語でプログラミングしていたことを考えると，型をはじめとした様々な抽象化機構によってスケーラビリティを獲得したことは偉大な発明であると感じます． Definitely Typed によって既存の JavaScript 資産を吸収するようなエコシステムを構築した点も，今後，多くの漸進的型付き言語が参考にするモデルになるだろうと思います．漸進的型付き言語の先駆けとして，今後どのように進化していくのか非常に楽しみなプログラミング言語です．

3.2. Python

Python（https://www.python.org/）は言わずと知れた動的型付き言語です． Python では PEP 484（https://www.python.org/dev/peps/pep-0484/）によって，型ヒント（一般に型アノテーションと呼ばれるもの）の文法が定義されています．その中には Any 型も定義されており，"Every type is consistent with Any" とあります．これはつまりAny がワイルドカードだということで，漸進的型付けを取り入れていることがわかります．非常に重要なのは，型ヒントの文法が公式に定義されただけで，特別な Python 処理系が作られたわけではないという点です．まず，型ヒントを加えたとしてもプログラムはそのまま実行することができます．これは TypeScript のような，型アノテーション等の文法を元の JavaScript 環境に持ち込めない言語と大きく異なる点です．また，型ヒントを書いて python コマンドでプログラムを実行したからといって静的型付けや最適化が行われることもありません．

静的型付けを行うための代表的なツールとしては mypy（http://mypy-lang.org）があります． mypy は PEP 484 の定義に基づいた型付けを行ってエラーを報告しますが，プログラムに変更を加えることはありません．ある種の Lint ツールのようなものだと Introduction には記述されています．

では，Python と mypy を組み合わせたものを漸進的型付き言語だと思ってみると，それは理論的に望ましい振る舞いをするかを考えます．上に述べたように mypy はプログラムに変更を加えることはありません．当然キャストのような新たな動的型検査の仕組みをプログラムに挿入しないので， TypeScript と同様に実行時に型が変化してしまう問題を抱えています．また，typeshed（https://github.com/python/typeshed）という， TypeScript で言う Definitely Typed にあたる型定義ファイルのリポジトリがありますが，まだまだ充実しているとは言い難く，サードパーティーのライブラリとの連携にも不安が残ります．

Python の漸進的型付けは TypeScript に比べるとまだまだ始まったばかりという印象を受けます．しかし，ここで注目しておきたいのは Python 自体に型ヒントの拡張が施されている点です． TypeScript のように派生した別の言語を作るのではなく，もとの言語に漸進的型付けを意図した拡張を施したことで，多くの人の関心を集めるきっかけになるのではないかと期待しています．また，型ヒントの文法のみを定義しそれをどのように使うかは他のツールに任せる，という問題の切り分け方も面白く，今後多くの先進的な型チェッカが現れることが期待されます．

3.3. なぜキャストが必要か

これまでの節で確認したように，TypeScript と Python の漸進的型付けに共通する問題は，「キャストに基づいた動的型検査の仕組みが存在しないこと」です．

しかし，ちょっと待ってください． JavaScript も Python も動的型付き言語で，動的型検査がないわけではありません． 2.1節の example4 のように実行時に型が変化してしまう可能性はありますが，それが原因でOSが落ちたり大事なレポートを書き換えたりしないように実装されているはずです．漸進的型付けも，わざわざキャストなどという新しいものを発明せずに，既存の動的型付き言語の仕組みに依存してはいけないのでしょうか．この節では，漸進的型付けと動的型付き言語の関係をもう少し詳しく見たあと，キャストをベースにした動的型検査の方が望ましい性質を持っているということを説明します．

example4 を少し変更した次のような例を見てみましょう．

function example5(x: string) : string {
    return x.concat("xyz");
}

var y : any = 42;

example5(y);

concat は文字列を連結するメソッドで，string 型の値には存在しますが， number 型の値には存在しないメソッドです．これを JavaScript に変換して実行すると，次のようなエラーが表示されます．

Uncaught TypeError: x.concat is not a function

42.concat という存在しないメソッドを呼び出そうとしたので undefined が返り，それを値に適用したので「x.concat は関数ではない！」と怒っています． string 型の引数を期待する example5 に number 型の値が渡ってしまっているのは確かですが，存在しないメソッドを呼び出そうとしたところで動的型検査が行われています．静的型付けで検出できないエラーを実行時に検出するという目的を達成しているようにも見えます．

しかし，次のような例をみると問題があることが分かります． example5 の関数本体を少しだけ充実させた例です．

function example6(x: string) : string {
    ...
    // x を用いない副作用を起こす処理
    ...
    return x.concat("xyz");
}

var y : any = 42;

example6(y);

example6 では，値を返す前にログを出力したりデータベースを書き換えるといった副作用を起こすものとしましょう．すると，example6 に number 型の値が渡るという明らかな型エラーがあるにも関わらず，不正なメソッド呼び出しをする前に example6 内の副作用が実行されてしまいます．ソフトウェアデザインにおける "Fail-fast" のポリシーを信じるのであれば，これはあまり嬉しい状況とは言えません．

2.2節で述べたようなキャスト挿入処理を行えば，上のような問題は簡単に回避することができます．挿入されたキャストをチェックすることで，値が example6 に渡る前に型エラーを検出できるということは以下のように簡単に確かめられます．

// キャスト挿入結果
function example6(x: string) : string {
    ...
    // x を用いない副作用を起こす処理
    ...
    return x.concat("xyz");
}

var y : any = (42 : number ==> any);

example6(y : any ==> string);
---> example6((42 : number ==> any) : any ==> string)
---> Runtime TypeError!

このように，静的型付け時に収集した型情報に基づいたキャストの方が，より早く実行時型エラーを検出できることがわかります．他にも，キャストにプログラム中の行番号を持たせるといった工夫をすることで，デバッグを容易にするような例外を投げるようなことも考えられます．もともとの動的型付き言語の機能を使って動的型検査を行うことはできますが，キャストをベースにした動的型検査がもたらす利益は大きく，実際の漸進的型付き言語でもそうした動的型検査を実装していくことは重要であると考えられます．

4. 漸進的型付けの目標

この章では，漸進的型付き言語が目指すべきゴールを段階的に示します．特に「既存の動的型付き言語を理論に沿って漸進的型付き言語に進化させる場合」について議論をすることに注意してください．既存の静的型付き言語に any 型を加えることでも漸進的型付き言語は生み出せますし，理論に沿った実行前後の型検査が実用上必ずしも必要というわけでもありません．この章の目的は，理論的視点から考えられる一つのフローチャートを示すことによって，漸進的型付けの未来を具体的に考えるための足がかりを得てもらうことです．それぞれの節では，まず達成すべき目標を簡単に説明し，その目標に関係の深いプログラミング言語に触れたあと，目標を達成する上での課題や難しいポイントを簡単に紹介します．

4.1. 静的型付けを行う

ある動的型付き言語を漸進的型付き言語に進化させたいと考えるなら，まずは静的型付けのことを考えなければいけません．型アノテーションをどのように文法に組み込むかといったところから，言語機能を十分に型付けするにはどんな型が必要で，どのようにチェックしたら良いのかといったことをひとつひとつ考えていく必要があります．

この段階の新たな取り組みとしては， RubyKaigi 2016 の基調講演*3 で述べられた Ruby の型付けの構想が記憶に新しいと思います． structural subtyping と型推論を組み合わせるようなアイディアを提示し，多くの人の関心を集めました．

この節で述べたいのは，TypeScript や Python の型付けがそれなりに上手く動いているからといって，決してこの段階の取り組みが簡単なわけではないということです． any 型と既存の言語機能を組み合わせることは非常に難しい問題で，理論のレベルでもまだまだ発展途上です．そもそも，動的型付き言語のあらゆる機能に any 以外の静的な型をつけることが可能なのかという疑問もあります．漸進的型付き言語の入り口である静的型付けですが，依然として多くの課題が残されています．

4.2. キャストによる動的型検査を行う

静的型付けのフェーズがある程度の完成をみたならば，次はキャスト等による動的型検査を考えなければいけません．この部分を既存の動的型付き言語の機能でまかなってしまうというのも一つの選択ではありますが，静的型付けで収集した型情報を利用した動的型検査に大きなメリットがあるのは 3.3節で確認した通りです．

この目標を目指す段階にあるプログラミング言語としては，TypeScript と Python が考えられます．非常に大きな開発コミュニティと，ある程度成熟した any 型を含む静的型付けを持ち合わせた数少ない言語であると思います．動的型検査を行うための試験的な実装は既に存在しており*4 *5， TypeScript や Python における動的型検査は実現可能なレベルに近づいています．

この目標を達成している言語としては，Scheme 系の方言である Racket の，そのまた方言である Typed Racket（https://docs.racket-lang.org/ts-guide/）があげられます．実行時に様々な仕様を検査できる契約（contract）システムをベースに，理論に近い動的型検査が実装されており，型のついた Typed Racket のモジュールと Racekt のモジュールを安全に組み合わせることが可能です．

この段階を達成するためのポイントは，ひとえに「キャストをどう実行するか」にあります．極端な例ですが，42 : number ==> string が成功するような動的型検査を実装しても望んだような結果は得られません．このシンプルな例では誰もが間違いに気がつきますが， any 型や複雑な型（例: 多相型）がキャストに現れた時に，どのようなキャストを許し，どのようなキャストを失敗させるのかということは，必ずしも簡単な問題ではありません．また，キャストに型エラー報告のための情報を付加することは以前から言われていますが，実際にどのような情報を乗せて，どのような形でプログラマに提示するのが良いのか，ということは議論の余地がある問題です．

4.3. 動的型検査を効率よく行う

キャスト挿入による動的型検査で型安全性を確保できたなら，次はその効率について考える必要があります．実行時に追加で型検査を行うのですから，多少のオーバーヘッドがあることは多くの人が想像できるはずです．では，そのオーバーヘッドは許容できるものでしょうか．例えば，最も基本的なキャスト計算をそのまま実装すると，再帰呼び出し回数に比例したメモリ領域を消費するケースが存在することが知られています．また，2016年の Typed Racket に関する研究では，型付きのモジュールと型なしのモジュールを相互に行き来するような一部のコードが， Racket で実行するよりも 100 倍近く遅くなることが報告されました *6．その後，多少の改善が行われたようですが，依然としてドキュメントにはオーバーヘッドに関する注意が記載されています．

漸進的型付けにおける動的型検査を効率よく行うことは最先端の研究課題です． TypeScript や Python，Typed Racket などを対象にした具体的な実装も研究されており， 4.2節で引用している実装にはそうした工夫も含まれています．これらを詳しく紹介することはこの記事が目指すレベルを大きく逸脱するため，ここでは割愛します．

この目的を達成するにあたって多くのことが試されています．以下にその中のいくつかを示します．

静的型付け時に制限を加えてキャストが少なくて済むようにする
キャストとは異なる戦略によって同様の動的型検査を達成する
JIT によって繰り返し実行される型検査を高速化する

4.4. 型情報に基づいて最適化を行う

動的型検査を効率よく実行できるようになったとしても我々の歩みは止まりません．ここまで考えてきた未来の漸進的型付けというのは，既存の動的型付き言語にキャストを追加する形で考えられているものが多いです．そのような実装では，どれほどキャストの効率をよくしたとしても，実行が遅くなることはあれど，実行が早くなるということはありません．キャストはオーバーヘッドを増やすことしかしないので当然です．型付けの保証を得るために必ず実行効率を犠牲にしなければいけないというのは面白くありません．実行前に収集した型情報を用いて，実行を早くすることはできないでしょうか．

例えば，Python の次のような実行を考えてみましょう．

> 1 + 1
2

非常にシンプルな計算ですが，背後ではとても複雑なことが起こっています．一般に，実行するまで + のオペランドがどんな型の値になるかは分からないので，実行時にオペランドの型を検査し，その後で実際に演算を実行したりエラーを送出したりします．これは漸進的型付けとは全く関係のない，Python の動的型付き言語としての振る舞いです． Python が C言語などと比較して遅いと言われる原因の一つでもあります．

しかし，漸進的型付けを導入して静的型付けを行うと，実行前にオペランドが int 型であるという情報を得ることができます．この情報をもとに，足し算の直前に行われていた型チェックを省略することはできないでしょうか．実行前の型情報を使って，初めから型チェックがいらないような表現で値を持っておいて， C言語に匹敵するような速度で Python を実行できたら面白いと思いませんか．

実際に，Typed Racket には型情報を使った最適化の機能があります． 4.3節で触れたのと同様の研究で，全てのモジュールに型をつけた場合に，わずかですが実行速度が上がったという結果が報告されています．他にも，nominal subtyping を持った非常にシンプルな漸進的型付き言語において，型情報による最適化を効かせるといった研究が発表されています*7．「型をつけるほどコードが早くなる」という夢のような世界はもう少し先ですが，漸進的型付けが目指すべき究極のゴールの一つであることには違いないでしょう．

5. 漸進的型付けの未来

この記事では，漸進的型付けの理論に基づいた現状の分析と今後の展望を述べました．まず，漸進的型付けの理論が any 型を用いた静的型付けとキャストによる動的型検査の二つのフェーズから構成されているということを説明しました．そのあとで，現状の漸進的型付けを取り入れているプログラミング言語がキャストによる動的型検査を欠いており，望ましい振る舞いが得られていないということを説明しました．最後に，「現在の動的型付き言語を理論に沿って漸進的型付き言語に進化させるとしたら」という観点から，大きく4つの目標を示しました．

漸進的型付けは，既存の動的型付き言語に対して様々な恩恵をもたらす可能性を秘めています．例えば，この記事で紹介した部分的な静的型付けや型情報を利用した最適化といったものです．くれぐれも，漸進的型付けを静的型付けの侵略だと思ってはいけません．漸進的型付けの魅力は，その名前の通り「漸進的な型付け」を許すことから，各言語の後方互換性を壊さないことにあります．一つの言語の中に，型を書きたい人と型を書きたくない人が共存することを可能にします．漸進的型付けは，既存の動的型付き言語にさらなる柔軟性を与えるための技術だとみなすことができるでしょう．

漸進的型付けは発展途上の技術であり，膨大な知恵と試行錯誤を必要としています．一人でも多くの人がこの記事を通して漸進的型付けに興味を持ち，その未来について考えを巡らせてくれたならば，とても嬉しく思います．

CAMPHOR- Advent Calendar 2017 12日目は @tomoyat1 の担当です．

*1:Siek et al. 2006. Gradual Typing for Functional Languages. Scheme And Functional Programming Workshop.

*2:Siek et al. 2015. Refined Criteria for Gradual Typing. SNAPL.

*3:http://rubykaigi.org/2016/presentations/yukihiro_matz.html

*4:https://github.com/mvitousek/reticulated

*5:Rastogi et al. 2015. Safe & Efficient Gradual Typing for TypeScript. POPL.

*6:Takikawa et al. 2016. Is Sound Gradual Typing Dead? POPL.

*7:Muehlboeck et al. 2017. Sound Gradual Typing Is Nominally Alive and Well. OOPSLA.

yu-i9.tmp

漸進的型付けの未来を考える