kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

PEP 483を読む

型ヒントをもうちょっと勉強しておこう
PEP 484よりもPEP 483の方が読む分には楽で面白く読めそうな気がするのでそっち読む

PEP 483 -- The Theory of Type Hints | Python.org

PEP 483 -- 型ヒントの理論

型理論、を意識したタイトルなんだろうか
TAPLを放置している自分には心が痛い

以下、引用のスタイルにしてますけど引用でもなく和訳ですらなくテキトーなまとめ
単に自分の感想と見分けが付くようにするためのマークと思ってください

この文書では、型ヒントの提案に関する理論を説明します。多くの詳細を決めていく必要があり、完全な提案や仕様ではありませんが、詳細な仕様を話し合うために必要な理論について説明していきます。

それくらいで十分です

おおざっぱな内容

型とは

ここでは、値の集合とそれらの値に適用できる関数の集合を型と呼びます。
型は様々な方法で適宜できます。
- 値を列挙する(TrueとFalseでbool、とか)
- 適用できる関数を与える(lenで長さを取得できる型、とか)
- class文を書く

組み合わせることによってさらに複雑な型も

このPEPの目的

タイプチェッカーが理解できる形で型を定義することが大事です。このPEPではPEP 3107で定められたシンタックスで変数や関数の型をアノテートすることをゴールとします。アノテーションはバグを防いだり、ドキュメントになったり、実行速度を揚げたりするのに使えますが、ここではバグを避けることに商店を置きます。

部分型の関係

静的タイプチェッカーで重要なのは、部分型の関係です。
first_varがfirst_typeという型を持ち、second_varがsecond_typeという型を持つとき、first_varにsecond_varを安全に代入できるためには

  • second_typeのあらゆる値がfirst_typeのの値の集合に属し、かつ
  • first_typeのあらゆる関数はsecond_typeの関数の集合に属する

ことが必要です。このような関係を部分型関係と言います。

実例

すべての犬は動物で、犬は鳴くなどより多くの関数を持ちます。したがって、犬は動物の部分型です。
整数は実数の部分型です。すべての整数は実数であり、ビットシフトなどより多くの関数を持ちます。

これは普通だしわかりやすい

ちょっとトリッキーな例を考えてみましょう。整数のリストは実数のリストの部分型では*ありません*。

とな?

第一の条件は満たしますが、実数をappendできるのは実数のリストだけですから、第二の条件を満たしません。

それはそうなんだけどそれを言ったら実数を足せるのは実数だけって
ことにならないか

def append_pi(lst: List[float]) -> None:
    lst += [3.14]

my_list = [1, 3, 5]  # type: List[int]

append_pi(my_list)   # 素直に考えると、これは成功するはず

my_list[-1] << 5     # でもこれが失敗する

これと何が違うかというと・・・?

>>> def plus_pi(a): return a + 0.5
>>> a = plus_pi(3)
>>> a << 5
TypeError: unsupported operand type(s) for <<: 'float' and 'int'

実際書いてみると、aははじめからfloat型としか書けないのか
つまりリストは関数で値が変わってしまうことがある、つまり
ミュータブルだからまずいけど
普通の整数はイミュータブルだから大丈夫、っていう違い?
あんまり自信なし

部分型の情報を宣言するには二通りのやり方があります。

公称型(Nominal Subtyping)では型のツリーはクラスツリーに基づきます。Pythonでは、互換性を保たないで属性を上書きすることができるので、このアプローチはタイプチェッカーのもとで行うべきです。

これは普通に型を宣言するタイプ

もうひとつは構造的部分型(Structural Subtyping)で、こちらは宣言されたメソッドから部分型関係を推論するものです。ときに混乱を呼びますが、構造的部分型はより柔軟と考えられています。公称型に加えて構造的部分型も用いることができるようにしようと努力しています。

こっちはこの説明だとちょっとよくわからなくて
型宣言を書かないで型を推論するよって話かと思ったけど
(そういう側面もあると思うけど)
ふたつの型を同様に扱えるなら同じ型とみなす的なものらしい
静的ダックタイピングって感じか

なるほど