本稿は Python に型アノテーションを追加するという PEP 483 - The Theory of Type Hinting の提案で参照されている Jeremy Siek (@jeremysiek) 氏と Walid Taha 氏が開発した漸進的型付けについての入門記事の翻訳です。
Python 3.5 で導入された型アノテーションについて興味がある方は以下を参考にしてください。
私自身、型システムに明るくないため、一部未訳の部分があったり、勘違いや誤訳もあると思います。そういった誤りを見つけたら編集リクエストを送ってもらえると助かります。
漸進的型付け (Gradual Typing) とは何か
漸進的型付けとは、私が 2006 年に Walid Taha とともに開発した型システムです。それはプログラムのある部分は 動的型付け で、他の部分は 静的型付け にするといったことを許容する型システムです。プログラマーは、どの部分から型アノテーションを除外するか、もしくは追加するかを制御します。本稿は漸進的型付けの優しい入門記事です。
以下が漸進的型付けを開発する我々の動機でした:
大規模なソフトウェアシステムは部分的に複数の言語で開発されることが多くなっています。これは動的型付け言語はある作業に向いていて、静的型付け言語はまた別の作業に向いているからです。漸進的型付けの型システムでは、プログラマーは静的型付けと動的型付けを選択できます。そこには別の言語に切り替えることや言語の相互運用性の痛みを伴うことはありません。願わくば、これがプログラマーの生産性を向上させるといいのにと思います。
いくつかの言語は、すでにオプションの型アノテーションを持っていますが、意外にも、型チェッカーがオプションの型アノテーションをどう処理すべきか、型システムはどういったことを保証すべきかといったことについての formal な取り組みはほとんど行われていませんでした。オプションの型アノテーションを持つ言語には Common LISP, Dylan, Cecil, Visual Basic.NET, Bigloo Scheme, Strongtalk があります。漸進的型付けは、これらの言語がオプションの型アノテーションで何をするかについての基盤を提供することを意味します。また Python 3, JavaScript の次のバージョン (ECMAScript 4) や Perl 6 といったオプションの型アノテーションを追加しようとしている新たな言語も開発中です。うまくいけば、我々の漸進的型付けの取り組みがこれらの言語に影響を与えるでしょう。
漸進的型付けを説明する前に、動的型付けと静的型付けを見直してみましょう。
動的型チェック
人気のある言語のうちいくつか、特にスクリプト言語は動的型付けされる言語です。例えば、Perl, Python, Javascript, Ruby や PHP などです。一般的には、 型 は一連の共通操作をもつ値の集合を記述するようなものです。例えば、int という型は、加算や減算といった操作を支援する (通常は32ビット) 数の集合を記述します。型エラー は、誤った型の値に対する操作に適用されるものです。例えば、整数に (文字列を) 連結しようとするとある言語では型エラーが発生します。その言語では、連結は文字列のみが行える操作です。型エラーの別の例としては、あるオブジェクトのメソッドを呼び出すときに発生します。それは car.fly() のように、そのオブジェクトが呼び出そうとするメソッドを実装していないときです。(空飛ぶ車が未だに主流になっていないのは残念ですね、もう 2000 年をとっくに過ぎたのに！)型エラー の正確な定義はプログラミング言語次第です。例えば、ある言語は整数と文字列の連結を許容するのを選択していて、別の言語はそうではありません。動的型付け言語では、型チェックがプログラムの実行中に行われます。それはオペランド型がその操作にとって適切かを保証するためにそれぞれの操作を適用する直前に行います。
以下は型エラーを発生させる Python のプログラムです。
def add1(x):
return x + 1
class A:
pass
a = A()
add1(a)
標準の Python インタープリターで上記のプログラムを実行すると次のように出力されます。
TypeError: unsupported operand type(s) for +: 'instance' and 'int'
(上記のエラーメッセージが、任意のクラスの ‘instance’ であると言う代わりに クラス ‘A’ のインスタンスだとより具体的になれば、素晴らしいでしょう。)
静的型チェック
Java, C#, C や C++ といった言語が静的にチェックされる言語として人気があります。静的にチェックされる言語では、プログラムを実行する前に型チェッカーが一部もしくは全ての型エラーさえも捕捉します。通常、型チェッカーはコンパイラの一部であり、コンパイル時に自動的に実行されます。
前節で紹介した例を Java に適用したプログラムを紹介します。
class A {
int add1(int x) {
return x + 1;
}
public static void main(String args[]) {
A a = new A();
add1(a);
}
}
このクラスをコンパイルすると、Java コンパイラは、次のメッセージを出力します。
A.java:9: add1(int) in A cannot be applied to (A)
add1(a);
^
1 error
特定のプログラムが実行されるときに型エラーが発生することを型チェッカーがどう予測するかについて疑問に思う人もいるでしょう。その答えは予測できないということです。プログラムが型エラーを発生させるかさせないかを一般的に予測する型チェッカーを構築するのは不可能です。(これは既知の停止性問題に相当します。)代わりに、全ての型チェッカーは実行中に起こることの保守的な近似を行い、型エラーを引き起こす かもしれない 何かについてのエラーメッセージを伝えます。例えば、Java コンパイラは実際には型エラーを発生させないにも関わらず、次のプログラムを拒否します。
class A {
int add1(int x) {
return x + 1;
}
public static void main(String args[]) {
A a = new A();
if (false)
add1(a);
else
System.out.println("Hello World!");
}
}
Java の型チェッカーは、実行時に通る if 文の分岐を把握しようとしません。その代わりに、保守的にどちらか一方の分岐先を通ると仮定し、それ故に両方の分岐先をチェックします。
動的型チェックと静的型チェックの比較
動的なチェックが優れていると思う人と静的型チェックが優れていると思う人との間で宗教戦争があります。この戦争があまりにも長い間行われている理由の1つは、両方のグループが良い点をもっているからだと私は考えています。(両方とも良くない点もいくつかあります。)残念ながら、一般的に2つのグループは他のグループがもつ良い点を良い点だと認めません。私の評価は以下の通りで、おそらく静的型付け支持者と動的型付け支持者のどちらも苛立たせるでしょう。無論、これらはそれぞれの視点についての議論、または反論があります。そして、以下の評価は私がその議論を検討した後で着地する場所を示します。
静的型チェックは、事前にバグを捕捉します。それ故に開発サイクルの後でバグ修正する多くのコスト、またはその場所で起こる多くのバグのコストさえも取り除きます。これは良い点です！ 動的型付けの支持者は、プログラムに対して徹底したテストスイートを作成することでより多くのバグを捕捉できると主張するでしょう。それでもなお、静的型チェックが型エラーを捕捉するために便利で低コストの方法を提供すると私は考えています。
動的型チェックはやりたいことを邪魔しません: 型チェッカーが受け入れるフォームへまずプログラムを変える必要がなく、そのプログラムをすぐに実行できます。 これは良い点です！ 静的型付けの支持者は、1) 実際にはそんな多くプログラムを変更する必要はない、または 2) 型チェッカーにあうように変更することがそのプログラムをより良く構造化されたものにする、のどちらかを主張するでしょう。1) が正しいと感じるプログラマーの理由は、使っている言語がプログラミングについての考え方を変えています。そして、どんな言語を使っても型チェックしてプログラムを書くようそれとなく仕向けます。また型システムのちょっと厄介なところを回避するのに慣れてしまいます。その型システムが厄介なものだというのを忘れて、代わりにその型システムを回避するノウハウに満足するようになります。2) に関しては、その型システムが最も明確で再利用可能なフォームのコードを表現するのに邪魔になるという状況があります。よく知られた Expression Problem がこの良い例です。型システムの研究が繁栄し続ける理由は、我々が書きたい全てのプログラムについて分かりやすく表せる、十分な表現力をもつ型システムを設計および実装することが困難だからです。
静的型チェックは高速な実行を可能にします。それは実行時に型チェックを行う必要がなく、値がより効率の良い表現で格納されるからです。これは良い点です！
動的型チェックは、値の型が実行時の情報に依存するといった状況に対応するのを簡単にします。これは良い点です！
静的型付けはモジュール性を向上させます。これは良い点です！ 例えば、動的言語だと、ライブラリのサブルーチンを不正に呼び出せますが、その後でそのルーチン内部の深いところで型エラーが発生します。静的チェックは、サブルーチンを呼び出したところで前もって型エラーを捕捉します。
静的型チェックは、バグをさらに減らすのに役立つプログラムについてより真剣に考えさせます。これは悪い点です。 型チェッカーはプログラムの単純なプロパティが適正であることのみをチェックします。プログラムが正しいことを保証する作業のほとんどは、静的型付けか動的型付けでチェックされる言語のどちらで記述されようと、包括的なテストを開発して検証します。
動的型チェックを使用すると、型アノテーションを書く時間を費やす必要はありません。 これは悪い点です。 型アノテーションを記述するのにかかる時間は全く取るに足らないもので、型アノテーションを必要とせず型チェックできる型推論と呼ばれるプログラムがあります。
静的型チェックと動的型チェックのどちらも一方が他方より普遍的に優れているとは言えないため、そういったパラダイムを強制せずプログラミング言語を切り替えるという選択肢をプログラマーに提供するのが理にかなっています。このことが漸進的型付けをもたらします。
漸進的型チェック
漸進的型チェッカー は、コンパイル時に型エラーを検出するためにプログラムを部分的にチェックしますが、他の部分はチェックしないといった型チェッカーです。それは型とともにアノテートされたプログラム部分により指示された通りにチェクします。例えば、Python 向けの我々の漸進的型チェッカーのプロトタイプは、上記のプログラムのエラーを伝えません。以下に再び記述します。
def add1(x):
return x + 1
class A:
pass
a = A()
add1(a)
しかし、プログラマーが以下のように引数 x に型アノテーションを追加するなら、型チェッカーはエラーを通知します。それは変数 a の型は A で、add1 関数の引数 x の型は int 型で不整合があるからです。
def add1(x : int):
return x + 1
class A:
pass
a = A()
add1(a)
(Python はローカル変数の宣言をもっていないため、a のようなローカル変数に対して静的な型を適用するための我々の規則は多少複雑です。しかし、ほとんどの場合は代入時の右辺の式と同じ型を変数に与えます。)
漸進的型チェッカーは、不明な型 (文字通り 動的 型とも呼ばれる) を与えることにより、アノテートされていない変数を扱います。それは任意の型から ? に、または ? から任意の型に暗黙の変換を許容することを "?" という文字で省略します。簡単にするために、+ 演算子はその引数が整数であるのを期待すると仮定します。漸進的型チェッカーは次の add1 関数を受け入れます。それは ? (x の型) から int (+ により期待される型) への暗黙の変換を許容するからです。
def add1(x):
return x + 1
? から int への暗黙の変換を許容することは安全ではなく、漸進的型付けに動的型付けの特性を与えるものです。ちょうど動的型付けと同様、x に束縛されるその引数は加算が実行される前にそれが整数型だと保証するために実行時にチェックされます。
前述したように、漸進的型チェッカーは任意の型から型 ? へ暗黙の変換も許容します。例えば、漸進的型チェッカーは add1 の次の呼び出を受け入れます。それは int (3 の型) から ? (引数 x の暗黙の型アノテーション) への暗黙の変換を許容するからです。
add1(3)
漸進的型チェッカーは、より複雑な型同士の暗黙の変換も許容します。例えば、次のプログラムには ? * int から int * int への異なるタプル型間の変換があります。
def g(p : int * int):
return p[0]
def f(x, y : int):
p = (x,y)
g(p)
一般的に、漸進的型チェッカーは2つの型間で相互に 一貫性がある なら暗黙の変換を許容します。我々は型 T と一貫性のある型 S を表現するために S ~ T という簡潔な表現を使います。2つの型が一貫性があるときに定義した規則をいくつか紹介します。
- 任意の型
Tについて? ~ TとT ~ ?の両方が成り立つ。 -
intのような任意の基本型BについてB ~ Bが成り立つ。 -
T1 ~ S1とT2 ~ S2な場合、タプル型T1 * T2は別のタプル型S1 * S2と一貫性がある。この規則は任意のサイズのタプル型に対して直接的な方法で一般化する。 -
T1 ~ S1…Tn ~ SnとR ~ Uの場合、関数型fun(T1,...,Tn,R)(T1…Tnは引数の型でRは返り値の型) は別の関数型fun(S1,...,Sn,U)と一貫性がある。
S と T の一貫性がないときは S !~ T と記述する。
従って、例えば以下のように記述する。
int ~ intint !~ bool? ~ intbool ~ ?int * int ~ ?fun(?,?) ~ fun(int,int)? ~ fun(int,int)int * int !~ ? * bool
なぜサブタイピングが機能しないのか
漸進的型付けは任意の型から ? への暗黙のアップキャストを許容します。それは Object 型がサブタイプ束 (subtype lattice) の上部にあるオブジェクト指向の型システムと似ています。しかし、漸進的型付けは暗黙のダウンキャストも許容するという点で異なります。これは漸進的型付けの際立った特徴であり、動的型付けの特性を与えるものです。Thatte の 準静的型付け (Quasi-static Typing) のような、静的型付けと動的型付けを混ぜるといった前述の試みはサブタイピングを使おうとしましたが、次の問題に対処する必要がありました。動的型がサブタイプ束のトップとボトムの両方として扱われる場合 (つまり暗黙のアップキャストとダウンキャストの両方を許容する場合)、サブタイピング関係が推移的であるためにその束は単一の要素しか持たない束へと崩壊します。言い換えれば、全ての型が他の全ての型のサブタイプになってしまい、型システムがプログラムを誤ったものとして棄却するということがもはやまったくできなくなってしまうのです。明らかな型エラーに対してでさえも、です。
次のプログラムを考えてみましょう。
def add1(x : int) -> int:
return x + 1
add1(True)
関数 add1 に対する引数として True を渡すのは明らかに型エラーですが、bool <: ? と ? <: int なら bool <: int が成り立ちます。このように、サブタイプベースの型システムは、このプログラムを受け入れるでしょう。Thatte は、型チェッカーの後に妥当性チェック (plausibility checking) という後処理 (post-pass) を追加することで部分的にこの問題に対応しました。しかし、Oliart が指摘したように、これは完全にアノテートされたコード内で全ての型エラーを捕捉するシステムには至りませんでした。私は Thatte の妥当性チェックの詳細には触れません。それはかなり複雑なようですが、ある例について議論します。次のプログラムは明らかな静的型エラーがありますが、それは妥当性チェックで検出されません。
def inc(x: number):
return x + 1
inc(True)
inc に対して True の適用は、inc と True の両方とも動的型 ? に暗黙的にアップキャストされます。その後 inc は ? -> ? に対して暗黙的にダウンキャストされます。妥当性チェッカーは number -> number と ? -> ? の最大下限のようにみえるため、警告なくこの問題を見過ごしてしまいます。