先日、Python の静的型チェッカーとして mypy を紹介しました。
私には難しくてまとめきれないため、Guido が参照している漸進的型付け (Gradual Typing) も含め、また別の機会に、、、。
とか言っているうちに1ヶ月ほど経ってしまいました。
そうこうしているうちに PEP のドラフトも出てきたので区切りとしてまとめておきます。一通り調べたことを基にして書いていますが、私の誤解や勘違いもあるでしょうから怪しいところがあったら調べ直してみてください。もちろんツッコミも大歓迎です。
型ヒント (Type Hints) を導入するという提案
現時点の PEP の内容をみて簡単にまとめます (これらはまだドラフトなので今後も内容が更新される可能性があります) 。
PEP 483 では、ここで言う型ヒントは、漸進的型付け (Gradual Typing) という型システムの理論体系に基づくものであり、その型システムがどういったものかという概要を説明しています。この PEP は漸進的型付けを導入するにあたっての原則や動機付け、その参照実装として mypy の構文を使った型アノテーションの具体例を紹介しています。型システムとしての側面に着目してその背景を整理したものにみえます。
そして、PEP 484 は PEP 483 の理論を実現するための型ヒントの標準化、それらの構文を提案するもののようです。ジェネリクスや直和型など動的型付けな型システムにはなかった概念や、プラットフォーム (OS やバージョン) に特化したチェックについての提案もあったりします。この PEP は先週に提案されたばかりというのもあり、メーリングリストや github でどういった構文や表現方法を受け入れるべきかといった議論がまさにいまも活発に行われています。
mypy から強く触発されているという冒頭の言葉もありますが、現時点の mypy では提供されていない Optional[T] を Union[T, None] と見なすといった記述もあります。mypy プロジェクトのブログによると、
作者である Jukka Lehtosalo 氏もその標準化の作業にコントリビュートしていると言っています。おそらくは、型ヒントを表現するために必要なものの大半は mypy に含まれる typing モジュールに実装し、そのモジュールを Python 3.5 から標準ライブラリのような形態で提供するように推測されます。念のために補足すると、これらの PEP で提案しているのは Python の型システムそのものに大きな変更を加えるのではなく、型ヒントに必要なものをなるべく Python モジュールで実現しましょうといった取り組みです。
PEP 484 を実現するために必要な issue が mypy のリポジトリにも登録されています。
これらの PEP を読んだ方の中には、型ヒントの標準化についての提案はあるけれど、それらが型チェッカーでどう扱われるかについては何も書いていないと思われた方もいるでしょう。mypy の作者の記事によると、これらの PEP は型ヒントの標準化を推めるものであって、それをどう扱うかは依然として型チェッカー (mypy も含む) や IDE、JIT コンパイラーといったサードパーティのツールやプロダクトに委ねるといった方針のようです。
PEP の最後にさらっとこんなことも書いてあります。
PEP 484 - Type Hints | Python.orgIs type hinting Pythonic?
Type annotations provide important documentation for how a unit of code should be used. Programmers should therefore provide type hints on public APIs, namely argument and return types on functions and methods considered public. However, because types of local and global variables can be often inferred, they are rarely necessary.
The kind of information that type hints hold has always been possible to achieve by means of docstrings. In fact, a number of formalized mini-languages for describing accepted arguments have evolved. Moving this information to the function declaration makes it more visible and easier to access both at runtime and by static analysis. Adding to that the notion that “explicit is better than implicit”, type hints are indeed Pythonic .
翻訳するとこんな感じでしょうか。
型ヒントは Pythonic か？
型アノテーションは、あるコードがどう使われるべきかという重要なドキュメントを提供します。それ故に、プログラマーはパブリックな API に型ヒントを提供すべきです。すなわちパブリックとみなす関数やメソッドの引数と返り値についてです。とはいえ、ローカル変数やグローバル変数の型は推論されるため、それらについての必要性はめったにないでしょう。
型ヒントのような類の情報は docstring で実現することも可能でしょう。実際のところ、受け取る引数を記述する形式化されたミニ言語もいくつか開発されました。この情報を関数定義へもっていくことは、実行時と静的解析時の両方においてアクセスしやすく、より見通しの良いものにします。さらに "暗黙よりも明示が良い" という考えからも、型ヒントはまさに Pythonic だと言えるわけです。
The Zen of Python からの引用はややこじつけな感もありますが、型ヒントもまた Pythonic という文化やイディオムを支えるものになっていくのかもしれません。
漸進的型付け (Gradual Typing) という型システム
PEP で参照されている漸進的型付けについてみてみましょう。Jeremy Siek 氏による 漸進的型付け の入門記事から要点をまとめます。
- 静的型付けと動的型付けの良いとこ取りをしようといった型システムである
- 漸進的型付けを備えた型システムでは、型を書く書かないを同一言語内で選択できる
- 型アノテーションを記述すると型チェッカーにより型エラーを捕捉できる
これは前述の PEP においては以下のように説明されています。
PEP 483 - The Theory of Type Hints | Python.orgSummary of gradual typing
We define a new relationship, is-consistent-with, which is similar to is-subclass-of, except it is not transitive when the new type Any is involved. (Neither relationship is symmetric.) Assigning x to y is OK if the type of x is consistent with the type of y. (Compare this to "... if the type of x is a subclass of the type of y," which states one of the fundamentals of OO programming.) The is-consistent-with relationship is defined by three rules:
- A type t1 is consistent with a type t2 if t1 is a subclass of t2. (But not the other way around.)
- Any is consistent with every type. (But Any is not a subclass of every type.)
- Every type is a subclass of Any . (Which also makes every type consistent with Any , via rule 1.)
That's all! See Jeremy Siek's blog post What is Gradual Typing for a longer explanation and motivation. Note that rule 3 places Any at the root of the class graph. This makes it very similar to object . The difference is that object is not consistent with most types (e.g. you can't use an object() instance where an int is expected). IOW both Any and object mean "any type is allowed" when used to annotate an argument, but only Any can be passed no matter what type is expected (in essence, Any shuts up complaints from the static checker).
翻訳すると、
漸進的型付けの概要
我々は is-consistent-with という新しい関係を定義します。それは新たな型 Any が適用されるときに推移的 (transitive)ではないという点を除けば、is-subclass-of の関係によく似ています。(これらの関係に対称性はありません。) もし x の型が y の型と一貫性がある (consistent) なら x を y に割り当てられます。(これを "もし x の型が y のサブクラスであるなら ..." という仮定に置き換えると、オブジェクト指向プログラミングの基礎の1つを述べています。) この is-consistent-with という関係は次の3つの規則で定義されます。
- 型 t1 が型 t2 のサブクラスなら型 t1 は 型 t2 と一貫性がある。(但し、その逆は成り立たない)
- Any は全ての型と一貫性がある。(但し、Any は全ての型のサブクラスではない)
- 全ての型は Any のサブクラスである。(規則1により、全ての型は Any と一貫性があるともみなせる。)
これが全てです！詳細な説明と動機付けは Jeremy Siek 氏のブログ記事 What is Gradual Typing を参照してください。規則3はクラスグラフの根 (root) に Any を置くということに注意してください。これは object にとてもよく似ています。その違いは object がほとんどの型と一貫性がないという点のみです (例えば、int が期待されるところで object() のインスタンスは使えません) 。言い換えると、Any と object の両方とも、ある引数をアノテートするときに使うには "任意の型を許容する" ことを意味しますが、どの型が期待されるかに関わらず引数に渡せるのは Any のみです (本質的には、Any は静的チェッカーからのメッセージを止める) 。
一貫性がある (is-consistent-with) という関係と Any という型が登場しています。この規則によると、全ての型の基底クラスであり、全ての型と一貫性のある任意の型として Any という型を定義しましょうとあります。ここで、この規則をよく見直してみると、型としての object と Any をあえて分けているのは何のためだろう？という疑問が出てきました。一見すると型としての object も Any の条件を満たせそうにもみえます。PEP には object との違いは一貫性の有無しか書いていません。
メーリングリストでのやり取りを検索してみたところ、おそらくは以下の操作に対する扱いが最も大きな違いではないかと推測します。
Also, consider the important difference between Any and object. They are both at the top of the class tree -- but object has *no* operations (well, almost none -- it has repr() and a few others), while Any supports *all* operations (in the sense of "is allowed by the type system/checker"). This places Any also at the *bottom* of the class tree, if you can call it that. (And hence it is more a graph than a tree -- but if you remove Any, what's left is a tree again.)
[Python-ideas] Type Hinting Kick-off
つまり、object 型はほとんどの操作をサポートしないけれど、Any は全ての操作をサポートするという点です。
def func(x: object) -> int: return x + 1 # object 型は + (__add__) という操作をサポートしない
こういったアノテーションの型チェックを行うときに具象型でもある object は型チェッカーからみたら扱いにくいのかもしれません。
>>> object() + 1 Traceback (most recent call last): File "<stdin>", line 1, in <module> TypeError: unsupported operand type(s) for +: 'object' and 'int'
漸進的型付けの入門記事では、漸進的型チェッカーが不明な型を 動的型 として扱うときに、そういった動的型に対するアップキャスト (派生クラスから基底クラスへのキャスト) とダウンキャスト (基底クラスから派生クラスへのキャスト) の両方を許容するというのが際立った特徴であると説明しています。そのため、サブクラスの関係は 動的型 をアップキャスト・ダウンキャストすることにより同じ型にキャストされてしまい、型チェックが機能しなくなるとあります。
そこで is-consistent-with という関係をもって型チェックするために上述した3つの規則を定義しました。ある型に対するサブクラスと Any は一貫性があると定義することにより、この問題を回避するというのが狙いです。そして object 型は全ての型の基底クラスとなるので一貫性がないという規則が導かれる、ということでしょうかね。
漸進的型付けを導入している言語として wikipedia には以下が紹介されています。ActionScript がこのカテゴリーに含まれるんだというのを知るとそう目新しいものでもないんだなと自身の勉強不足を実感しました。
Examples of gradually typed languages include ActionScript, Dart, Dylan, Hack, Perl 6, Typed Racket, Typed Clojure, TypeScript, and mypy (a static type checker for Python).
wikipedia:en:Gradual_typing
ちょうど Dylan という言語コミュニティでも漸進的型付けについての記事が投稿されていました。
Python の型システムに対する懸念
Flask などの開発者として知られる Armin Ronacher 氏の記事から紹介します。
彼はフレームワークやライブラリの開発経験から API の設計において型システムがどういったものであることを望むかという視点を述べています。いまの動向から未来のプログラミング言語は、強力な型システムを備えていて、なお柔軟性や生産性を保持するといったものになると考察しています。Python という言語は、そのインタープリターの実装である CPython の最適化や歴史的経緯により課題を抱えています。具体的には C 言語側か Python 側かのどちらで実装されるかで型意味論が異なるという状況になっており、そのことは PyPy といった他処理系の実装や API 設計に悪影響を及ぼすと懸念を抱いています。
過去または現在も抱えている CPython の型システムの不明瞭さから、Python に型アノテーションを導入することよりも型システムをより強力なものに改善すべきだというのが彼の想いのようです。とはいえ、これから Python の型システムを改善しようというのは多大な時間と労力がかかることから現実的には無理だろうというのも理解しています。mypy や漸進的型付けへの言及はあまりないことから、型アノテーションの導入には興味がないといったようにみえます。
以前の mypy を紹介した記事においても PyPy のコア開発者である Alex Gaynor 氏も同様のことを示唆していました。
PyPy で良いことがあるんじゃないかと妄想しますが、PyPy のコア開発者である Alex Gaynor は、型アノテーションが PyPy にとって価値がないと断言しています。彼は型アノテーションの導入よりも、Python の型システムを改善しようと提案していますが。
mypy で静的型付け Python プログラミング - forest bookPS: You're right. None of this would provide *any* value for PyPy.
[Python-ideas] Proposal: Use mypy syntax for function annotations
Python の作者である Guido van Rossum 氏からのメーリングリストでのやり取りをみる限り、互換性を崩さずに型アノテーションを導入していこうといった姿勢が伺えました。現在の Python ほどの規模のユーザーコミュニティになると、Armin 氏や Alex 氏が指摘するような型システムの改善という、影響範囲の大きそうな改善を期待するのは難しいのかもしれません。その視点からも mypy で実装された型アノテーションが既存の Python 3 の構文としてそのまま実行可能であるというのは特筆すべきことなのだと思います。
型アノテーションと Composability の考察
Andrew Montalenti 氏による記事を紹介します。
彼は、関数アノテーションが導入された当時からアノテーションに対する Composability *1 が欠けていると指摘しています。関数アノテーションには階層化の機構がなかったため、フレームワークによって記述方法が異なったり、そのことが可読性を落とすものになり得ると考えているようです。
例えば、以下のような関数アノテーションの定義方法を比較した場合、
def foo( *args: {"doc": "arguments", "type": list}, **kwargs: {"doc": "keyword arguments", "type": dict}): \ -> {"doc": "a bar instance", "type": Bar}
アノテーションデコレーター を使う Pyanno: Python Annotations の例を紹介しながら
from geometry import Point @returnType(float) @parameterTypes(Point, Point) def getDistance(p1, p2): """ getDistance() calculates the distance between two points. """ ...
一目瞭然であると説明しています。
彼の提案としては、アノテーションを階層化する仕組みと基本的な慣習を提供するというものであったようです。(アノテーションの) 構文を変えずにその上に composition 層を設けるというのであれば、それはコードの明瞭さにはつながらない。そして、いまはアノテーションの用途をドキュメント利用に限定した方が良いのではないかと指摘しながら、mypy の構文は簡潔で表現力のあるものだという点も認めていて、議論の開始点としては良さそうだとも述べています。
最後に
But let’s remember: simple is better than complex — and practicality beats purity!
» Python annotations and type-checking
という The Zen of Python からの言葉で締めくくっています。
Composability という概念
Andrew 氏の記事に対する lawrence 氏のトラックバックも読んでみました。彼は Composability が指すものはこういうものではないかと考察しています。
Python に対する mypy は、実行時にプログラムの動作に影響を与えないため、Clojure に対する Typed Clojure とよく似ています。動的型付き言語に型チェックを追加することは、形式的ではなくユニットテストに必要なもののを多くをアサートできるのに加え、ドキュメントとして役立つので、一定の間違いを防げるというのが彼の経験談のようです。さらに composable とはどういうものだろう？という問いに Shen という実験的言語の機能から、真に composable な型システムは、ある型の規則が別の新たな型定義の一部に使えるものだと説明しています。
最後に Andrew 氏の意味する composable を誰にでも分かるように言い換えると、Clojure ではデータ型の定義とドキュメントとしてのアノテーションの定義は別になっており、その両方を兼ねようとしている Python の型アノテーションは悪い考えだと締めくくっています。
型システムにまつわる用語
型システムについて調べているときに用語が分からなくて苦労したので少し整理しておきます。
選択的型付け (Optional Typing, Optional type systems)
- Optional type systems
- c# - Is there a language that allows both static and dynamic typing? - Stack Overflow
漸進的型付けと関連して似たような意図を表すのに使われるそうですが、厳密には違う定義のようです。基本的には wikipedia の受け売りです。
大きな違いは漸進的型付けは同一言語内で型の有無を選択しようという意図に対して、選択的型付けは型システムの選択と言語の選択を独立させて、必要に応じて言語内にモジュールであるかのように型システムを組み込むことを示唆しています。但し、現実的には型がその言語の動作に影響しないという要件を実現するのは難しく、例えば、クラスベースの継承はできないことになってしまうとあります。
型ヒント (Type Hinting, Type Hints)
私がググった限りでは、厳密な定義をみつけることはできませんでした。おそらくは言葉通りの用語の意味でしかないと思います。
Clojure が型ヒントと選択的型付け (または漸進的型付け) という2つの用語を使い分けています。
Clojure には言語機能として型ヒントの仕組みがあります。これは実行時のリフレクションを避けることでプログラムの最適化を行うことを目的としていて、型エラーを捕捉するといった用途には使えません。
(defn len [x] (.length x)) (defn len2 [^String x] (.length x)) user=> (time (reduce + (map len (repeat 1000000 "asdf")))) "Elapsed time: 3007.198 msecs" 4000000 user=> (time (reduce + (map len2 (repeat 1000000 "asdf")))) "Elapsed time: 308.045 msecs" 4000000
Python の PEP でも型ヒントという用語を使っていますが、いまのところ、最適化には使われません。型アノテーションをドキュメントもしくは型チェッカーのための用途だと明言して型ヒントと呼んでいるため、Clojure で言う型ヒントと Python で言う型ヒントは異なる用途を指す用語となっています。
そして、選択的型システム (または漸進的型付け *2 ) を導入する仕組みとして Typed Clojure (Python でいう mypy) があります。ann というマクロで関数アノテーションを指定できるようです。
(ann add [Number -> Number]) (defn add [x] (+ x 1))
リファレンス:
まとめ
まとめられないですね ... (´・ω・｀)
今回扱った話題の中には、型システム、構文、コミュニティなどプログラミング言語に関するいろんな知見を含んでいました。いくつか記事を読んだだけでは自分の中に明確なモデルを構築できなかったのと、自分の解釈が正しいかどうかを検証するのが難しいというのも分かりました。それでも良かったことは、他のプログラミング言語について知るきっかけになったことです。
Python へ型ヒントのための構文や仕組みを導入すること自体は、私が調べた限りでは、一定数の支持は得ていて積極的に進められているようにみえます。Python の型システムに懸念があるというのは、おそらくはその通りなのでしょうけれど、型ヒントの導入とは直接関係するものではないので分けて考えた方が良いように思いました。
