問題意識の所在
自作クラスを宣言するときに、定義するクラスが用いるデータ型に制約を与えるだけでなく、そのクラスのインスタンスが持ちうる値の範囲や、長さの範囲についても制約を与えることができる言語は、依存型や篩型の型クラスを宣言できる言語として、知られています。篩型は、「ふるい」型と読みます。
データ型に「要素数」や「長さ」といった数的な制約条件を持ち込むことで、どんな実用的なご利益があるのか？という素朴な疑問に答える上で、次の記事が参考になります。
型に値を埋め込むだけだとありがたみがないですが、カリー＝ハワード同型対応で「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)といわれているので、証明をやるにはリッチな型が必要なのです。
依存型が何に役に立つのか
依存型の応用には以下のものがあります。他にもあると思いますが。
- プログラムの証明 -Coq, Agdaなどの定理証明支援システム
- 固定長の配列、行列
- Deep Learningで使うテンソルの次元を型に埋め込むケース
- 実装例
- haskellによるpythonのtensorflowのラッパ
- 配列の次元を型に埋め込むケース
- vector-sized
- clash-prelude
- スーパーモナド
- ステートを型に埋め込むケース
- アドベントカレンダーの10日の記事の指標付きモナド
- idrisの例
- データベースのスキーマ
- OuryさんとSwierstraさんのものがあるらしいが、こちらに例があります。
IdrisやLiquidHaskell、v6.11以降のRacket言語などのプログラミング言語は、依存型と篩型を宣言し、静的な型検査を行うことができる言語です。
・Dependent Types と Refinement Types の違い
・Refinement Types For Haskell
・型をさらに拡張するーーRefinement Typesについて
・LiquidHaskell のインストールと学習方法
・Liquid Haskell で普通の型システムの上を行け #NGK2017B
foo :: { x:a | P x } -> { y:b | Q y }a 型のうち条件 P を満たす値から b 型のうち条件 Q を満たす値への関数
（Liquid Haskellではない通常の）Haskellにも、拡張機能（extension）として、依存型を利用可能にする動きがあります。
- CLaSH.Sized.Vector
- - Data.Vector.Storable.Sized
- dependent haskell Adding dependent types to Haskell
- Why Dependent Haskell is the Future of Software Development
- Dependent type
また、Scalaでも、次のWebページで解説されているように、篩型の型クラスを宣言できる機能がすでに実装されているようです。
・ (GitHubリポジトリ）fthomas/refined
・ refinedで値が満たすべき条件を型で表現する
： 「さらなる型安全性を求めて ~ Refinement TypeをScalaで実現する ~」
refinedとは
refinedはRefinement Type(篩型)をScalaで実現するためのライブラリで、既存の型に対して型レベルで満たすべき条件を指定することで、取りうる値を制限することができます。もともとはHaskellの同名のライブラリを移植したもののようです
ScalaでRefinement Typeを扱えるrefinedライブラリを使った実装例については、@wcsakuraiさんの記事がQiitaにあります。
・ 「恵比寿のおすすめランチスポットAPIをfinchで書く(scala/finch/circe/refined)」
Pythonでも、型アノテーションの導入（typingモジュール）や、静的な型検査を行うことができるmypyが登場する流れを受けて、データ型の型チェックを行うだけでなく、データ値の値の範囲や配列の長さを型チェックの文脈で、静的にチェックできないか、調べてみました。
その結果、Pythonで依存型と篩型の型クラスを宣言できるようにするスクリプトが、GitHubで公開されていました。
・ (GitHubリポジトリ）vixrant/python-type-theory
以下のstackoverflowでのやり取りから、見つけたものです。
・ Can Python implement dependent types?
So, can we implement a type Vect, which can be used as in
def append(a: Vect[m, T], b: Vect[n, T]) -> Vect[(m+n), T]:
return a + b
, where m and n are natural numbers, and T is any type?
I made a library which allows you to treat types as first-class, without hard-coding in advance like David said. Of course, it's hacky too, rewriting functions to make use of type hints.
https://github.com/vixrant/python-type-theory
git cloneして、使ってみたところ、うまく動きました。
% git clone https://github.com/vixrant/python-type-theory
Cloning into 'python-type-theory'...
remote: Enumerating objects: 79, done.
remote: Counting objects: 100% (79/79), done.
remote: Compressing objects: 100% (61/61), done.
remote: Total 79 (delta 36), reused 50 (delta 18), pack-reused 0
Unpacking objects: 100% (79/79), done.
%
ここでは、git cloneで取得したディレクトリにcdして作業をおこないます。
任意の階層パスのディレクトリから、取得したPythonスクリプトファイルを使うためには、パスを通す必要があります。
・ @derodero24さんのQiita記事「【Python】自作モジュールへのパスの通し方」
今回は、パスは通さないで進めます。
% ls -lt | head
total 2920
drwxr-xr-x 8 Afoguard staff 256 11 25 21:40 python-type-theory
% ls -lt python-type-theory
total 32
-rw-r--r-- 1 Afoguard staff 537 11 25 21:40 sample.py
-rw-r--r-- 1 Afoguard staff 2083 11 25 21:40 refinement.py
-rw-r--r-- 1 Afoguard staff 1398 11 25 21:40 ast_rewrite.py
-rw-r--r-- 1 Afoguard staff 2532 11 25 21:40 README.md
%
iPythonの対話型インタプリタを立ち上げます。
git cloneしたPythonスクリプトは、内部でinspect.getsource()メソッドを呼び出すのですが、Pythonの対話型インタプリタでこのメソッドを使うと、inspect.py, raise OSError('could not get source code')エラーが起きるためです。
iPythonの対話型インタプリタは、このエラーを発生させずに、inspect.getsource()メソッドを使うことができるようです。
なお、iPythonを使わずに、Python2系やPython3系を使う場合でも、Pythonのスクリプトファイルを実行する場合は、OSエラーを発生させずに、今回 git cloneしたモジュールを使うことができます。
（ 参考 ）
・teratail 「Pythonで対話インタプリタ上で宣言した関数の実装を見る方法」
それでは、冒頭のgithubリポジトリに掲げられているサンプルコードを実行して、挙動を確認します。
型検査テスト１（ 成功 ）
% cd python-type-theory
Afoguard% ipython
Python 3.9.0 (default, Nov 19 2020, 22:16:24)
Type 'copyright', 'credits' or 'license' for more information
IPython 7.19.0 -- An enhanced Interactive Python. Type '?' for help.
In [1]:
@reftypeデコレータを付けて、次のメソッドを定義してみます。
・メソッド名：N
・ 「0よりも値の大きい、int型オブジェクト」であるかどうかを判定するメソッド
このメソッドの帰り値は、TrueかFalseのboolean値です。
In [1]: from refinement import refine, reftype
In [2]: @reftype
...: def N(i: int) -> bool:
...: return i > 0
...:
In [3]:
これで、自作クラスであるN型（クラス）が定義できました。
このクラスは、「0よりも値の大きい、int型オブジェクト」だけを持つことができます。
それでは、コンストラクタに、「0よりも小さい値を持つint型オブジェクト」（負の符号を持つ整数）-4_を渡して、N型のインスタンスを生成してみます。
In [3]: x = N(-4)
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-3-aff855616743> in <module>
----> 1 x = N(-4)
~/Desktop/python-type-theory/refinement.py in wrf(v)
49 def wrf(v):
50 if not wf(v):
---> 51 raise TypeError(f"Value {v} does not satify refinement {f.__name__}")
52 return v
53
TypeError: Value -4 does not satify refinement N
In [4]:
結果は、期待した通り、次の型エラーが発生しました。
TypeError: Value -4 does not satify refinement N
それでは、N型の型制約条件を満たす「0よりも小さいint型オブジェクト」である4（正の符号を持つ整数）_を渡して、N型のインスタンスを生成してみます。
In [4]: x = N(4)
In [5]: print(type(x))
<class 'int'>
In [6]: print(x)
4
In [7]:
無事に「4」の値を持つN型のインスタンスが生成されました。
型検査テスト2（ 成功 ）
次に、先ほどと同じように、@reftypeデコレータを付けて、「文字数が0よりも大きくて、（なお且つ）大文字で始まるstr型オブジェクト」であるかどうかを判定するメソッド CapitalisedNameを自作します。
このメソッドの帰り値は、TrueかFalseのboolean値です。
In [7]: @reftype
...: def CapitalisedName(s: str) -> bool:
...: return len(s) > 0 and s[0].isupper()
...:
In [8]:
これで、自作クラスであるCapitalisedName型（クラス）が定義できました。
このクラスは、「文字数が0よりも大きくて、（なお且つ）大文字で始まるstr型オブジェクト」だけを持つことができます。
それでは、コンストラクタに、「小文字で始まる文字列（str型オブジェクト）」である'vikrant'を渡して、CapitalisedName型のインスタンスを生成してみます。
In [8]: y = CapitalisedName('vikrant')
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-9-ca75b8144c65> in <module>
----> 1 y = CapitalisedName('vikrant')
~/Desktop/python-type-theory/refinement.py in wrf(v)
49 def wrf(v):
50 if not wf(v):
---> 51 raise TypeError(f"Value {v} does not satify refinement {f.__name__}")
52 return v
53
TypeError: Value vikrant does not satify refinement CapitalisedName
In [9]:
結果は、期待した通り、次の型エラーが発生しました。
TypeError: Value vikrant does not satify refinement CapitalisedName
「大文字で始まり、文字数が0（文字）より大きい文字列（str型オブジェクト）」である'Vikrant'をコンストラクトに渡すと、
型エラーを発生させることなく、CapitalisedName型インスタンスを生成させることができます。
In [9]: y = CapitalisedName('Vikrant')
In [10]: print(type(y))
<class 'str'>
In [11]: print((y))
Vikrant
In [12]:
自作した型制約付きのクラスを用いて、メソッドを定義してみる
型制約を満たす値をコンストラクタに渡した場合のみ、自作クラスからインスタンスを生成することができることが分かりました。
では、次に、「取りうる値」に制約を持つ自作型クラスを、自作メソッドを定義するときに付ける型アノテーションの中で用いてみます。
今度は、@refineデコレータを付けます。
ここでは、githubリポジトリにあるサンプルコードを少し変えてみました。
In [13]: @refine
...: def greet(name: CapitalisedName, dept: str, age: N) -> str:
...: return f"{name} さんは、 {dept}に所属する {age} 歳の社員です。"
...:
In [14]:
メソッドが定義できました。
それでは、第１引数"name"に、CapitalisedName型のインスタンスを渡して、greetメソッドを呼び出して実行してみます。
In [14]: message = greet("Charles", "Python編集部", 37)
In [15]: print(type(message))
<class 'str'>
In [16]: print(message)
Charles さんは、 Python編集部に所属する 37 歳の社員です。
無事に動きました。
第１引数"name"に、小文字で始まる文字列を渡すと、CapitalisedName型が持つ「大文字で始まる」という値制約を破るため、エラーが発生します。
TypeError(f"Value {v} does not satify refinement {f.name}")が発生します。
(satifyはsatisfyの誤字だと思われます）
In [17]: message = greet("charles", "Python編集部", 37)
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-37-ae44d4c694b2> in <module>
----> 1 message = greet("charles", "Python編集部", 37)
~/Desktop/python-type-theory/refinement.py in wrapped(*args, **kwargs)
23 if k not in predicates:
24 continue
---> 25 predicates[k](v)
26
27 # Run the refined function
~/Desktop/python-type-theory/refinement.py in wrf(v)
49 def wrf(v):
50 if not wf(v):
---> 51 raise TypeError(f"Value {v} does not satify refinement {f.__name__}")
52 return v
53
TypeError: Value charles does not satify refinement CapitalisedName
In [18]:
次に、「大文字で始まり、文字数が7文字未満である」文字列という値の制約を持つ自作型クラスLengthRestrictedStringを定義してみます。
In [18]: @reftype
...: def LengthRestrictedString(s: str) -> bool:
...: return len(s) < 7 and s[0].isupper()
...:
In [19]:
7文字を超える文字数の文字列を、定義したLengthRestrictedString型コンストラクタに渡してみます。
エラーが発生しました。意図した通りです。
In [20]: new_string = LengthRestrictedString("Having eaten too much, I came to feel so bad.")
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-42-c36e9d6a3330> in <module>
----> 1 new_string = LengthRestrictedString("Having eaten too much, I came to feel so bad.")
~/Desktop/python-type-theory/refinement.py in wrf(v)
49 def wrf(v):
50 if not wf(v):
---> 51 raise TypeError(f"Value {v} does not satify refinement {f.__name__}")
52 return v
53
TypeError: Value Having eaten too much, I came to feel so bad. does not satify refinement LengthRestrictedString
In [21]:
7文字を超えない文字数の文字列を、定義したLengthRestrictedString型コンストラクタに渡してみます。
こちらも意図した通り、エラーを出さずに、LengthRestrictedString型のインスタンスが生成できました。
In [21]: new_string = LengthRestrictedString("Bad.")
In [22]: print(type(new_string))
<class 'str'>
In [23]: print(new_string)
Bad.
In [24]:
配列（List）の長さに制約を与える方法
GitHubレポジトリでは、次のサンプルコードが掲載されています。
In [35]: @refine
...: def MinLenList(lim: N):
...: @reftype
...: def LenLimit(l: list) -> bool:
...: return len(l) >= lim
...: return LenLimit
...:
In [36]:
In [37]: test_list
Out[38]: ['a', 'abc', 'd']
MinLenList()メソッドに3を与えて、要素数が３以上のリストかどうかを検査するメソッド（返り値はbool型）を定義します。
In [39]: lengh_condiiton_checker_func = MinLenList(3)
In [40]: print(type(lengh_condiiton_checker_func))
<class 'function'>
次に、配列オブジェクトtest_listを与えてみます。
In [41]: result = lengh_condiiton_checker_func(test_list)
In [42]: print(result)
['a', 'abc', 'd']
test_listは、要素数が３つで、MinLenList(3)型の型制約を満たすので、MinLenList(3)型のインスタンスの生成に成功しました。
次に、要素数が3より少ない配列を与えてみます。
In [43]: test_list2 = [1, 2]
In [44]: lengh_condition_checker_func2 = MinLenList(3)
In [45]: result2 = lengh_condiiton_checker_func2(test_list2)
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-95-f28c0af3b174> in <module>
----> 1 result2 = lengh_condiiton_checker_func2(test_list2)
~/Desktop/python-type-theory/refinement.py in wrf(v)
49 def wrf(v):
50 if not wf(v):
---> 51 raise TypeError(f"Value {v} does not satify refinement {f.__name__}")
52 return v
53
TypeError: Value [1, 2] does not satify refinement LenLimit
In [46]:
意図した通り、エラーが発生しました。
配列の要素がすべて同じデータ型であるという制約は与えていないので、要素数が３個以上の配列でありさえすれば、型制約は満たします。
In [47]: test_list3 = [1, 2, 'f', 9, 10, 15, 1]
In [48]: lengh_condition_checker_func3 = MinLenList(3)
In [49]: result = lengh_condiiton_checker_func3(test_list3)
In [50]: result3 = lengh_condiiton_checker_func3(test_list3)
In [51]: print(result3)
[1, 2, 'f', 9, 10, 15, 1]
In [52]:
それでは、定義したlengh_condiiton_checker_func3型クラスを、自作メソッドの型アノテーションの中で用いてみます。
自作メソッドが受け取る第２引数に、lengh_condiiton_checker_func3型クラスのインスタンスを受け取るよう定義しました。
In [53]: @refine
...: def greet(name: str, scores: lengh_condiiton_checker_func3, age: N) -> str:
...: return f"{age} 歳の{name}さんのスコア履歴は、{scores}です。"
...:
In [54]:
In [55]: message = greet("Charles", [1, 'a'], 37)
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-108-28e9986b9cad> in <module>
----> 1 message = greet("Charles", [1, 'a'], 37)
~/Desktop/python-type-theory/refinement.py in wrapped(*args, **kwargs)
23 if k not in predicates:
24 continue
---> 25 predicates[k](v)
26
27 # Run the refined function
~/Desktop/python-type-theory/refinement.py in wrf(v)
49 def wrf(v):
50 if not wf(v):
---> 51 raise TypeError(f"Value {v} does not satify refinement {f.__name__}")
52 return v
53
TypeError: Value [1, 'a'] does not satify refinement LenLimit
In [56]:
第２引数に要素数が２つしかない配列を渡したため、意図した通り、第2引数の型制約を満たさないというエラーが発生しました。
次に、要素数が4の配列を第2引数に渡してみます。
In [57]: message2 = greet("Charles", [1, 'a', 'b', 100], 37)
In [58]: print(message2)
37 歳のCharlesさんのスコア履歴は、[1, 'a', 'b', 100]です。
In [59]:
要素数が4の配列は、lengh_condiiton_checker_func3型クラスの値制約を満たすため、今度は実行に成功しました。
配列の長さ（要素数）に制約を与える：失敗コード事例
以下は実行エラーになった。
In [24]: @reftype
...: def UpperBoundedList(l: list, upper_length_num : int) -> bool:
...: return (len(l) < upper_length_num)
...:
---------------------------------------------------------------------------
AssertionError Traceback (most recent call last)
<ipython-input-46-3cc4954bbae0> in <module>
1 @reftype
----> 2 def UpperBoundedList(l: list, upper_length_num : int) -> bool:
3 return (len(l) < upper_length_num)
4
~/Desktop/python-type-theory/refinement.py in reftype(f)
37 def reftype(f: types.FunctionType):
38 assert type(f) == types.FunctionType, "Predicate should be a function"
---> 39 assert len(f.__annotations__) == 2, "Predicate should type hint the input parameter, the output should be bool"
40 assert f.__annotations__['return'] == bool, "Predicate should return a boolean value"
41
AssertionError: Predicate should type hint the input parameter, the output should be bool
In [25]:
以下もエラー
In [26]: from typing import List, Sequence, TypeVar
In [27]: T = TypeVar('T')
In [28]: @reftype
...: def LengthUpperBoundedList(l: [T], n: int) -> T:
...: return (len(l) < n)
...:
---------------------------------------------------------------------------
AssertionError Traceback (most recent call last)
<ipython-input-52-1ea0ca96cec8> in <module>
1 @reftype
----> 2 def LengthUpperBoundedList(l: [T], n: int) -> T:
3 return (len(l) < n)
4
~/Desktop/python-type-theory/refinement.py in reftype(f)
37 def reftype(f: types.FunctionType):
38 assert type(f) == types.FunctionType, "Predicate should be a function"
---> 39 assert len(f.__annotations__) == 2, "Predicate should type hint the input parameter, the output should be bool"
40 assert f.__annotations__['return'] == bool, "Predicate should return a boolean value"
41
AssertionError: Predicate should type hint the input parameter, the output should be bool
In [29]:
In [30]: @reftype
...: def func_(x, n: int) -> bool:
...: condition = (len(x) < n)
...: return condition
...:
In [31]:
In [32]: test_list = ['a', 'abc', 'd']
In [33]: result = func_(test_list, 7)
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
<ipython-input-80-3ea8e98e2aa1> in <module>
----> 1 result = func_(test_list, 7)
TypeError: wrf() takes 1 positional argument but 2 were given
In [34]: