型システムの概念¶
静的型付け、動的型付け、および逐次型付け¶
静的型付け プログラミング言語は、プログラムを実行する前に型チェッカーを実行します。 プログラムは、言語の型システムに従って型が正しいことが求められます。 型システムは、言語内のすべての式に型を割り当て、それらの使用が型付けルールに従っていることを検証します。 通常、型が正しくないプログラム(つまり、型エラーを含むプログラム)は実行されません。 Java および C++ は、静的型付けのオブジェクト指向言語の例です。
動的型付け プログラミング言語は、プログラムを実行する前に型チェッカーを実行しません。 代わりに、実行時に操作を実行する前に値の型をチェックします。 これは、言語が「型なし」であることを意味するわけではありません。 実行時の値には型があり、その使用は型付けルールに従います。 すべての操作がチェックされるわけではありませんが、属性アクセスや算術などの言語の特定の基本操作はチェックされます。 Python は動的型付け言語です。
逐次型付け は、静的型付けと動的型付けを組み合わせる方法です。 型注釈付きの Python は、細かい粒度で静的型チェックをオプトインすることを可能にし、プログラムを実行せずに一部の型エラーを静的に検出できます。 変数、パラメータ、および戻り値には、オプションで静的型注釈を付けることができます。 単一のデータ構造の型内でも、静的型チェックはオプションであり、細かい粒度で行われます。 たとえば、辞書はキーの型の静的チェックを有効にし、値の型の動的ランタイムチェックのみを持つように注釈を付けることができます。
逐次 型システムは、特別な「不明」または「動的」型を使用して、静的に型が不明な名前または式を記述する型システムです。 Python では、この型は Any と表記されます。 Any は静的に不明な型を示すため、静的型チェッカーは Any として型付けされた式の操作の型の正しさをチェックできません。 これらの操作は、Python ランタイムの通常の動的チェックを介して引き続き動的にチェックされます。
Python の型システムは、呼び出し可能 型内および tuple[Any, ...]``(:ref:`tuples` を参照)内で ``... を使用して、型の静的に不明なコンポーネントを示します。 これらの使用に関する詳細なルールは、それぞれの仕様のセクションで説明されています。 これらをまとめて、Any とともに、逐次形式 と呼びます。
この仕様は、Python の逐次型システムを説明しています。
完全に静的な型と逐次型¶
サブパートとして 逐次形式 を含まない型を 完全に静的な型 と呼びます。
逐次型 は、完全に静的な型、Any 自体、またはサブパートとして逐次形式を含む型のいずれかです。 すべての Python 型は逐次型です。 完全に静的な型はそのサブセットです。
完全に静的な型¶
完全に静的な型は、潜在的なランタイム値のセットを示します。 たとえば、完全に静的な型 object は、すべての Python オブジェクトのセットです。 完全に静的な型 bool は、値のセット { True, False } です。 完全に静的な型 str は、すべての Python 文字列のセットです。 より正確には、ランタイム型(__class__ 属性)が str または str から直接または間接的に継承するクラスであるすべての Python オブジェクトのセットです。 Protocol は、特定の属性および/またはメソッドのセットを共有するすべてのオブジェクトのセットを示します。
オブジェクト v が完全に静的な型 T によって表されるオブジェクトのセットのメンバーである場合、v は型 T の「メンバー」である、または v は T を「含む」と言えます。
逐次型¶
Any は、未知の静的型を表します。 これは、未知のランタイム値のセットを示します。
これは、すべての Python オブジェクトのセットを表す完全に静的な型 object に似ているように見えるかもしれませんが、まったく異なります。
式が object 型を持つ場合、静的型チェッカーは、式の操作がすべての Python オブジェクトに対して有効であることを確認するか、静的型エラーを発行する必要があります。 これにより、非常に少ない操作が許可されます! たとえば、x が object として型付けされている場合、x.foo は静的型エラーであるべきです。なぜなら、すべての Python オブジェクトが foo 属性を持っているわけではないからです。
一方、Any として型付けされた式は、_いくつかの_ 特定の静的型を持つと仮定する必要がありますが、_どの_ 静的型が不明です。 静的型チェッカーは、Any がエラーを回避する静的型を表す可能性がある場合、式または文の操作に対して静的型エラーを発行しないでください。 (これは、具現化と代入可能性の観点から、以下でより正確に定義されています。)
同様に、 tuple[int, Any] (タプル を参照)や int | Any (共用体型 を参照)などの型は、単一のオブジェクトのセットを表しません。 代わりに、許容されるオブジェクトのセットの範囲を表します。
同じように、Any が「すべての Python オブジェクトのセット」を表すのではなく「不明なオブジェクトのセット」を表すように、tuple[int, Any] は「最初の要素が整数である長さ 2 のすべてのタプルのセット」を表しません。 それは完全に静的な型であり、tuple[int, object] と表記されます。 対照的に、tuple[int, Any] は、タプル値の不明なセットを表します。 それは、整数と文字列のタプルのセット、または整数と文字列のタプルのセット、または他のタプル値のセットである可能性があります。
実際には、この違いは、たとえば、tuple[int, Any] 型の式を tuple[int, int] として型付けされたターゲットに代入できるという事実に見られますが、tuple[int, object] を tuple[int, int] に代入することは静的型エラーです。 (再び、具現化と代入可能性の定義でこの違いを正式にします。)
同じように、完全に静的な型 object が Any に対する可能なオブジェクトのセットの上限であるように、完全に静的な型 tuple[int, object] は tuple[int, Any] に対する可能なオブジェクトのセットの上限です。
逐次保証¶
Any は、動的に型付けされたプログラムに静的型を段階的に追加することを可能にします。 完全に動的に型付けされたプログラムでは、静的チェッカーはすべての式に Any 型を割り当て、エラーを発行しないでください。 プログラムに静的型を追加するか、型注釈を追加する(プログラムをより静的に型付けする)と、プログラムが正しくない場合や静的型がランタイム型を完全に表すことができない場合に静的型エラーが発生する可能性があります。 型注釈を削除する(プログラムをより動的にする)と、追加の静的型エラーが発生しないはずです。 これは通常、逐次保証 と呼ばれます。
Python の型システムでは、逐次保証を厳密な要件としては取りませんが、有用なガイドラインです。
サブタイプ、スーパータイプ、および型の同値性¶
完全に静的な型 B は、別の完全に静的な型 A の サブタイプ です。 これは、B によって表される値のセットが A によって表される値のセットのサブセットである場合に限ります。 セットのサブセット関係が推移的で反射的であるため、サブタイプ関係も推移的です(C が B のサブタイプであり、B が A のサブタイプである場合、C は A のサブタイプです)および反射的(A は常に A のサブタイプです)。
スーパータイプ 関係はサブタイプの逆です。 A は B のスーパータイプです。これは、B が A のサブタイプである場合に限ります。 または同等に、A によって表される値のセットが B によって表される値のセットのスーパーセットである場合に限ります。 スーパータイプ関係も推移的で反射的です。
完全に静的な型に対して 同値 関係も定義します。 型 A と B は同値(または「同じ型」)です。これは、A が B のサブタイプであり、B が A のサブタイプである場合に限ります。 これは、A によって表される値のセットが B によって表される値のスーパーセットおよびサブセットの両方であることを意味し、A と B は同じ値のセットを表す必要があります。
型 B が型 A よりも「狭い」(または「適切なサブタイプ」)であると言うことができます。 B が A のサブタイプであり、B が A と同値でない場合です。 同じシナリオでは、型 A が B よりも「広い」、または B の「適切なスーパータイプ」であると言うことができます。
名義型と構造型¶
str などの型(または他のクラス)は、__class__ が str であるか、直接または間接的に str から継承するクラスである値のセットを記述します。 サブタイプは直接サブクラス化に対応します。 str のサブクラス MyStr は str のサブタイプです。なぜなら、MyStr は str によって表される値のサブセットを表すからです。 このような型は「名義型」と呼ばれ、この「名義サブタイプ」です。
他の型(例:プロトコル および TypedDict)は、代わりに属性およびメソッドの型、または辞書キーおよび値の型によって値のセットを記述します。 これらは「構造型」と呼ばれます。 構造型は、スーパータイプとの継承またはサブクラス化関係がなくても、スーパータイプのすべての要件を満たし、さらに追加することによって、スーパータイプの可能な値のサブセットを表すため、別の型のサブタイプである場合があります。 これは「構造サブタイプ」です。
型によって表される値のセットを指定する手段は異なりますが、基本的な概念は名義型と構造型の両方に対して同じです。 型は可能な値のセットを表し、サブタイプはその値のサブセットを表します。
具現化¶
Any は未知の静的型を表すため、静的型に関する上記のサブタイプ、スーパータイプ、または同値関係のドメインには含まれません。
逐次型をより一般的に関連付けるために、具現化 関係を定義します。 具現化は、「より動的な」型を「より静的な」型に変換します。 逐次型 A が与えられた場合、A 内の 1 つ以上の Any の出現をいくつかの型(Any の各出現に対して異なる型である可能性があります)に置き換えると、結果の逐次型 B は A の具現化です。 (... を任意の型シグネチャに置き換えることにより、呼び出し可能 型を具現化し、決定長タプル型に置き換えることにより tuple[Any, ...] を具現化することもできます。)
たとえば、tuple[int, str]``(完全に静的な型)および ``tuple[Any, str]``(逐次型)はどちらも ``tuple[Any, Any] の具現化です。 tuple[int, str] も tuple[Any, str] の具現化です。
B が A の具現化である場合、B は A よりも「より静的な」型であり、A は B よりも「より動的な」型であると言えます。
具現化関係は推移的で反射的であるため、逐次型に対して前順序を定義します。
一貫性¶
具現化に基づいて、逐次型に対する 一貫性 関係を定義します。
完全に静的な型 A は、別の完全に静的な型 B と一貫性があります。これは、同じ型(A が B と同値である)である場合に限ります。
逐次型 A は逐次型 B と一貫性があり、B は A と一貫性があります。これは、A と B の両方の具現化である完全に静的な型 C が存在する場合に限ります。
Any はすべての型と一貫性があり、すべての型は Any と一貫性があります。 (これは具現化と一貫性の定義から導き出されますが、明示的に述べる価値があります。)
一貫性関係は推移的ではありません。 tuple[int, int] は tuple[Any, int] と一貫性があり、tuple[Any, int] は tuple[str, int] と一貫性がありますが、tuple[int, int] は tuple[str, int] と一貫性がありません。
一貫性関係は対称です。 A が B と一貫性がある場合、B も A と一貫性があります。 それはまた反射的です。 A は常に A と一貫性があります。
代入可能な関係(または一貫したサブタイピング)¶
具現化関係とサブタイピング関係を考慮して、すべての型に対する 一貫したサブタイプ 関係を定義できます。 型 B は、型 A の一貫したサブタイプです。これは、A の具現化 A' と B の具現化 B' が存在し、A' と B' が両方とも完全に静的な型であり、B' が A' のサブタイプである場合に限ります。
一貫したサブタイピングは、Python の代入可能性を定義します。 式は、変数の型注釈(それぞれ、パラメータの型注釈または戻り型注釈)の一貫したサブタイプである場合、変数に代入できます(関数に渡されるか、関数から返されるかを含む)。
型 B が型 A に「代入可能」であると言えます。 B が A の一貫したサブタイプである場合です。 この場合、A が B から代入可能であるとも言えます。
この仕様の残りの部分では、「一貫したサブタイプ」よりも 代入可能 という用語を好むことがよくあります。 2 つは同義ですが、「代入可能」の方が短く、多くの読者にとってより明確な直感を伝えるかもしれません。
たとえば、Any は int に assignable です。なぜなら、int は Any の具現化であり、int は int のサブタイプだからです。 同じ具現化は、int が Any に代入可能であることも示しています。
代入可能な関係は一般的に対称ではありません。 B が A のサブタイプである場合、tuple[Any, B] は tuple[int, A] に代入可能です。なぜなら、tuple[Any, B] は tuple[int, B] に具現化でき、これは tuple[int, A] のサブタイプだからです。 しかし、tuple[int, A] は tuple[Any, B] に代入可能ではありません。
逐次構造型の場合、一貫性と代入可能性も構造的です。 たとえば、「型 Any の属性 x を持つすべてのオブジェクト」の構造型は、「型 int の属性 x を持つすべてのオブジェクト」の構造型と一貫性があり(および代入可能)です。
型関係の要約¶
サブタイプ、スーパータイプ、および同値関係は、完全に静的な型に対して部分順序を確立します。 逐次型に対する類似の関係(具現化を介して)は、「代入可能」(または「一貫したサブタイプ」)、「代入可能」(または「一貫したスーパータイプ」)、および「一貫した」です。 この類推を次の表で視覚化できます。
完全に静的な型 |
逐次型 |
|---|---|
|
|
|
|
|
|
逐次型に対しても同値を定義できます。 2 つの逐次型 A と B は同値です(つまり、同じ逐次型であり、単に一貫しているだけではありません)。これは、A のすべての具現化が B の具現化でもあり、B のすべての具現化が A の具現化でもある場合に限ります。
属性とメソッド¶
Python では、ランタイムでオブジェクトに対して名前に代入する、関数に渡す、または関数から返す以上のことができます。 属性を取得/設定し、メソッドを呼び出すこともできます。
Python データモデルでは、値に対して実行できる操作はすべてメソッド呼び出しにデシュガーされます。 たとえば、a + b は(いくつかの詳細を省略して大まかに言えば)``type(a).__add__(a, b)`` または type(b).__radd__(b, a) の構文糖衣です。
静的型チェッカーの場合、a.foo において a の型が表すオブジェクトのすべてが foo 属性を持っていない限り、a.foo は型エラーです。 (__getattr__ の実装をすべての属性名のゲッターと見なし、同様に __setattr__ および __delattr__ も見なします。 複雑さ があります。属性アクセスの完全な仕様は独自の章に属します。)
完全に静的な型 A によって表されるすべてのオブジェクトが foo 属性を持っている場合、型 A が foo 属性を持っていると言えます。
A の型が逐次型である場合、単一のオブジェクトのセットを表さない場合があります。 この場合、a.foo は、A の具現化が foo 属性を持たない限り、型エラーです。
同様に、a の型が foo 属性を持つ型に代入可能でない限り、a.foo は型エラーです。
共用体型¶
単一の引数に対して予想される型の小さな制限されたセットを受け入れることは一般的であるため、型システムは | 演算子を使用して共用体型をサポートします。 例:
def handle_employees(e: Employee | Sequence[Employee]) -> None:
if isinstance(e, Employee):
e = [e]
...
完全に静的な共用体型 T1 | T2 は、T1 および T2 が完全に静的な型である場合、T1 および T2 によってそれぞれ表される値のセットの和集合によって形成される値のセットを表します。 したがって、スーパータイプ関係の定義により、共用体 T1 | T2 は T1 および T2 の両方のスーパータイプであり、T1 および T2 は両方とも T1 | T2 のサブタイプです。
逐次共用体型 S1 | S2 は、S1 および S2 が逐次型である場合、S1 および S2 の具現化によってそれぞれ表される可能な値のセットの和集合によって形成される可能なすべての値のセットを表します。
S1 の具現化を T1 に、S2 の具現化を T2 にする場合、S1 | S2 も T1 | T2 に具現化できます。 したがって、逐次型 S1 および S2 は両方とも逐次共用体型 S1 | S2 に代入可能です。
B が A のサブタイプである場合、B | A は A と同値です。
このルールはサブタイプにのみ適用され、代入可能には適用されません。 共用体 T | Any はより単純な形式に簡略化できません。 これは、下限 T を持つ未知の静的型を表します。 つまり、これは object と同じくらい大きい、または T と同じくらい小さいが、それより小さくないオブジェクトの未知のセットを表します。
同等の逐次型は、共用体から簡略化できます。 例:list[Any] | list[Any] は list[Any] と同値です。 同様に、共用体 Any | Any は Any に簡略化できます。 2 つの未知のオブジェクトのセットの和集合は未知のオブジェクトのセットです。
None との共用体¶
共用体型の一般的なケースの 1 つは、None との オプション 型です。 例:
def handle_employee(e: Employee | None) -> None: ...
型 Employee または None の型のいずれかが Employee | None の共用体に代入可能です。
この仕様の過去のバージョンでは、デフォルト値が None である場合にオプション型を仮定することを型チェッカーに許可していました。 例::
def handle_employee(e: Employee = None): ...
これは次のように扱われます。:
def handle_employee(e: Employee | None = None) -> None: ...
これはもはや推奨される動作ではありません。 型チェッカーは、オプション型を明示的にすることに向かって進むべきです。
共用体内のシングルトン型のサポート¶
シングルトンインスタンスは、特に None が変数の有効な値である場合に、特定の条件を示すために頻繁に使用されます。 例:
_empty = object()
def func(x=_empty):
if x is _empty: # デフォルト引数値
return 0
elif x is None: # 引数が提供されていて、それが None である場合
return 1
else:
return x * 2
このような状況で正確な型付けを許可するために、ユーザーは標準ライブラリによって提供される enum.Enum クラスと組み合わせて共用体型を使用する必要があります。 これにより、型エラーを静的に検出できます。:
from enum import Enum
class Empty(Enum):
token = 0
_empty = Empty.token
def func(x: int | None | Empty = _empty) -> int:
boom = x * 42 # これは型チェックに失敗します
if x is _empty:
return 0
elif x is None:
return 1
else: # この時点で型チェッカーは x が int 型であることを知っています
return x * 2
Enum のサブクラスはさらにサブクラス化できないため、上記の例のすべてのブランチで変数 x の型を静的に推論できます。 より多くのシングルトンオブジェクトが必要な場合も同様のアプローチが適用されます。 1 つ以上の値を持つ列挙を使用できます。:
class Reason(Enum):
timeout = 1
error = 2
def process(response: str | Reason = '') -> str:
if response is Reason.timeout:
return 'TIMEOUT'
elif response is Reason.error:
return 'ERROR'
else:
# response は str のみであり、他の可能な値はすべて使い果たされました
return 'PROCESSED: ' + response
参考文献¶
ここで紹介する概念は、逐次型付けの研究文献に由来しています。 例を参照してください。:
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual Typing: A New Perspective. Proc. ACM Program. Lang. 3, POPL, Article 16 (January 2019), 112 pages
Victor Lanvin. A semantic foundation for gradual set-theoretic types. Computer science. Université Paris Cité, 2021. English. NNT : 2021UNIP7159. tel-03853222