nikkie-ftnextの日記

イベントレポートや読書メモを発信

"型ヒントの簡単な導入"と言われる「PEP 483 -- The Theory of Type Hints」を読む（その1 Subtype relationships）

はじめに

頑張れば、何かがあるって、信じてる。nikkieです。
この週末（11/14, 15）、PEP 483 -- The Theory of Type Hints を読んでみました。
読んだ時に控えたメモを数回に分けてアウトプットします。

目次

なぜ読んだか

11/20(金)にはんなりPythonでLTが控えています1。
PEP 585（組み込みGeneric型2）について、登壇駆動でキャッチアップしようと申し込みました。
LTの準備として、型ヒントまわりのドキュメントを読んでみることにしました。
恥を忍んで言えば、型ヒントはドキュメントを読み込まず、雰囲気でやっている勢3でした。🙈

typingモジュールのドキュメントの冒頭に

型ヒントの簡単な導入は PEP 483 を参照してください。

とあるのを見つけ、PEP 483を読むことにしました。

注意事項

  • 翻訳ではありません。読んだときのメモです。なるべくPEP本体と対応するように進めます
    • 私の理解のためのメモ📝は斜体で追加します
    • 元の文章の斜体は太字にしています
  • 誤読と思われる箇所はコメントやTwitterでお知らせください。大変ありがたいです

検証環境

$ sw_vers
ProductName:    Mac OS X
ProductVersion: 10.14.6
BuildVersion:   18G4032
$ python -V
Python 3.8.6
$ mypy --version
mypy 0.790

PEP 483とは

タイトルは「型ヒントの理論」。
Abstractによると、「PEP484が参照する理論をはっきり説明する」もの。

著者はGuidoさんとIvanさんで、2014年12月に作られました。

Introduction

Python3.5向けの新しい型ヒントのプロポーザルをはっきり説明する（詳細には多く立ち入らない）

説明すること

  1. 理論の基本概念を思い出すことから始める（←この記事ではここだけ扱います）
  2. gradual typing（漸進的型付け）
  3. 一般的なルールを述べ、Unionのようなアノテーションで使われる新しく特殊な型を定義する
  4. Generic型（generic types4）と、型ヒントの実用面を定義する

表記の慣例

  • t1, t2やu1, u2は型。t1, ... のいずれかとしてtiと表記する
  • TやUは型変数（TypeVar()(Document)で定義される）
  • オブジェクト5、class文で定義されるクラス、PEP 8の慣例に従って示されるインスタンス
  • 型に適用される == は、このPEPでは、2つの式が同じ型であることを表す
  • PEP 484では、型は型チェッカー向けの概念で、クラスはランタイムの概念と区別する。本PEPでは区別を明らかにするが、型チェッカーの実装の柔軟性のために不必要な厳密性は避ける

Background

型という概念にはいくつも定義がある

  • 値の集合で定義する（値を列挙）
    • bool型：True, False
  • 値に適用できる関数の集合で定義する
    • Sized型：__len__メソッドを持つオブジェクト6
  • 単なるクラス定義による。intを継承したUserIDクラスの例（このクラスの全てのインスタンスはUserIDという型を形成する）
class UserID(int):
    pass
  • より込み入った例：int, strまたはそれらのサブクラスのインスタンスのみを含む全てのリストをFancyList型と定義（[1, "abc", UserID(42)]はFancyList型）

Subtype relationships（サブタイプ関係）

静的型チェッカーに対して決定的な関係がサブタイプ関係。
次の質問から生じる：
first_type型の変数first_varと、second_type型の変数second_varがあるとき、first_var = second_varという代入は安全（safe）か？

安全であるときの強い基準：

  • second_typeのどの値もfirst_typeの値の集合に含まれる、かつ
  • first_typeのすべての関数7はsecond_typeの関数の集合に含まれる

この関係をサブタイプ関係と呼ぶ。

📝上記は、「second_typeがfirst_typeのサブタイプ関係にある」の定義
📝second_typeがfirst_typeのサブタイプ関係にあるとき、first_var = second_varという代入は安全である。

上記の定義より、

  • 全ての型は、自身のサブタイプ
  • サブタイプ化が進むに連れ、値の集合は小さくなり、関数の集合は大きくなる

例

(1) first_typeをAnimal、second_typeをDogとする。
DogはAnimalのサブタイプ（📝 ＝Dog型の変数をAnimal型の変数に代入できる animal = dog）

📝なぜなら、以下のように「second_typeがfirst_typeのサブタイプ関係にある」の定義を満たすから

  • Dog型（second_type）の値（種々のわんこ🐶）であれば、Animal型（first_type）の値の集合（動物たち）に含まれる
  • Dog型（second_type）はbarkメソッドのようにAnimal型（first_type）よりも多くの関数を持つので、Animal型のすべての関数はDog型の関数の集合に含まれる

逆に、AnimalはDogのサブタイプではない

(2) 整数は実数のサブタイプである。

  • 全ての整数は実数でもある（📝＝second_typeのどの値（整数）もfirst_typeの値（実数）の集合に含まれる）、かつ
  • 整数はシフト演算8 << や >> のように多くの演算をサポートする（＝📝first_type（実数）のすべての関数はsecond_type（整数） の関数の集合に含まれる）

📝つまり「second_typeがfirst_typeのサブタイプ関係にある」を満たしている

lucky_number: float = 3.14
lucky_number = 42  # intはfloatのサブタイプなのでsafe
lucky_number * 2
lucky_number << 5  # PEP483では「Fails」ですが、mypyはスルー。どういうことでしょう？🤔

unlucky_number: int = 13
unlucky_number << 5
unlucky_number = 2.72  # unsafeなので、error: Incompatible types in assignment (expression has type "float", variable has type "int")

(3) List[int]型はList[float]型のサブタイプではない

List[int] は整数だけを含む全てのリストから構成される型を意味する。
List[float]は実数だけを含む全てのリストから構成される型を意味する。

  • 📝List[int]型の値は、List[float]型の値の集合に含まれる（＝second_type（List[int]）のどの値もfirst_type（List[float]）の値の集合に含まれる）
  • しかし、実数を末尾に追加する関数はList[float]でのみ機能する（→📝first_type（List[float]）のすべての関数はsecond_type（List[int]）の関数の集合に含まれるわけではない）
from typing import List


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


my_list: List[int] = [1, 3, 5]
append_pi(my_list)  # error: Argument 1 to "append_pi" has incompatible type "List[int]"; expected "List[float]"
my_list[-1] << 5  # mypyで検出されるので、実行時のエラーを避けられる

型チェッカーにサブタイプの情報を宣言する方法

型チェッカーにサブタイプの情報を宣言する方法は2つのアプローチが普及している

(A) nominal（名目的） subtyping
クラス木（class tree）に基づくタイプ木（type tree）
例：UserIDはintのサブタイプと見なせる（📝UserIDはintを継承したクラス9だから）
Pythonでは互換性のないやり方で属性をオーバーライドできるので、このアプローチが型チェッカーの管理のもとで使われるべき

class Base:
    answer = "42"


class Derived(Base):
    answer = 5  # error: Incompatible types in assignment (expression has type "int", base class "Base" defined the type as "str")

(B) structural（構造的） subtyping
宣言されたメソッドからサブタイプの関係にあるか推論する
例：UserIDとintは同じ型と見なされる
時折混乱を招くが、こちらはより柔軟と見なされている

アプローチ両方とも10にサポートを提供する。
nominal subtypingに加えて、 structural information（構造的な情報）も利用できる

終わりに

1の内容は以上になります。
Generic型の共変・反変を除いて、一通り読んでいるので、時間を見つけて続きを上げていきます。

サブタイプ関係にあるかどうかを考えていると、大学時代の数学の講義を思い出しました。
ふだん使っているプログラミング言語と学問体系のつながりの一端を実感できました。

  1. お時間ありましたらどうぞ。Python3.9について語るLT会です 【オンライン】はんなりPython #34 python3.9を語る LT会 - connpass↩

  2. python.jpの Python 3.9の新機能 - python.jp が分かりやすいと思います。PEP 483や他のドキュメントと行き来して、ようやく分かってきました↩

  3. ドキュメントを読むと、アンチパターンに手を出していたことが分かりました。知らないって怖いですね↩

  4. genericの訳が難しいですね。python.jpにならって「Generic型」としています。typingのドキュメントでは「ジェネリクス」となっているところもあります↩

  5. このObjectsは何がかかるのか今ひとつ分かっていません↩

  6. https://docs.python.org/ja/3/library/collections.abc.html#collections.abc.Sized↩

  7. 原文はevery function from first_type。メソッドも関数と理解しています↩

  8. https://docs.python.org/ja/3/reference/expressions.html#shifting-operations↩

  9. BがAを継承している（BはAのサブクラス）とき、「B型のどの値もA型の値の集合に含まれ」、かつ、（継承しているから）B型に適用できる関数はA型より増えるのでサブタイプ関係にあると結論付けられますね↩

  10. この部分の強調はnikkieによる↩