Pythonで関数型言語の依存型と篩型の型クラスを宣言する方法


##問題意識の所在

自作クラスを宣言するときに、定義するクラスが用いるデータ型に制約を与えるだけでなく、そのクラスのインスタンスが__持ちうる値の範囲や、長さの範囲についても制約を与える__ことができる言語は、__依存型や篩型の型クラスを宣言できる言語__として、知られています。篩型は、「ふるい」型と読みます。

__データ型に「要素数」や「長さ」といった数的な制約条件を持ち込むことで、どんな実用的なご利益があるのか？という素朴な疑問__に答える上で、次の記事が参考になります。

- [@junjihashimoto@githubさん 「依存型の紹介と応用としてのClashの紹介」](https://qiita.com/junjihashimoto@github/items/31f245f5e0138e5fac7e)

> 型に値を埋め込むだけだとありがたみがないですが、カリー＝ハワード同型対応で「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)といわれているので、証明をやるにはリッチな型が必要なのです。
>
>__依存型が何に役に立つのか__
>依存型の応用には以下のものがあります。他にもあると思いますが。
>
> - プログラムの証明
>   -Coq, Agdaなどの定理証明支援システム
> - 固定長の配列、行列
>   - Deep Learningで使うテンソルの次元を型に埋め込むケース
>      - 実装例
>      - haskellによるpythonのtensorflowのラッパ
>   - 配列の次元を型に埋め込むケース
>      - vector-sized
>      - clash-prelude
> - スーパーモナド
>     - ステートを型に埋め込むケース
>       - アドベントカレンダーの10日の記事の指標付きモナド
>       - idrisの例
>   - データベースのスキーマ
>      - OuryさんとSwierstraさんのものがあるらしいが、こちらに例があります。

__*[Idris](https://qiita.com/tags/idris)*__や__*[LiquidHaskell](https://qiita.com/tags/haskell)*__、__v6.11以降の*[Racket](https://qiita.com/tags/racket)*言語__などのプログラミング言語は、依存型と篩型を宣言し、静的な型検査を行うことができる言語です。

・[Dependent Types と Refinement Types の違い](https://7colou.red/blog/2018/07-07-difference/index.html)
・[Refinement Types For Haskell](https://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf)
・[型をさらに拡張するーーRefinement Typesについて](http://bugrammer.hateblo.jp/entry/2016/07/21/152813)
・[LiquidHaskell のインストールと学習方法](https://haskell.e-bigmoon.com/posts/2018/03-03-liquidhaskell-intro.html)
・[Liquid Haskell で普通の型システムの上を行け #NGK2017B](https://www.slideshare.net/y_taka_23/liquid-haskell-ngk2017b-83162127)
> ```foo :: { x:a | P x } -> { y:b | Q y }``` a 型のうち条件 P を満たす値から b 型のうち条件 Q を満たす値への関数

（Liquid Haskellではない通常の）Haskellにも、拡張機能（*extension*）として、依存型を利用可能にする動きがあります。

- [CLaSH.Sized.Vector](http://hackage.haskell.org/package/clash-prelude-0.11.2/docs/CLaSH-Sized-Vector.html)
- - [Data.Vector.Storable.Sized](http://hackage.haskell.org/package/vector-sized-0.6.1.0/docs/Data-Vector-Storable-Sized.html)
- [dependent haskell Adding dependent types to Haskell](https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell)
- [Why Dependent Haskell is the Future of Software Development](https://serokell.io/blog/why-dependent-haskell)
- [Dependent type](https://wiki.haskell.org/Dependent_type)

また、__[Scala](https://qiita.com/tags/scala)__でも、次のWebページで解説されているように、__篩型の型クラスを宣言できる機能がすでに実装__されているようです。

・ [(GitHubリポジトリ）fthomas/refined](https://github.com/fthomas/refined)
・ [refinedで値が満たすべき条件を型で表現する](https://dev.classmethod.jp/articles/refined-scala/)
： [「さらなる型安全性を求めて ~ Refinement TypeをScalaで実現する ~」](https://engineering.visional.inc/blog/168/scala-refined-newtype/)

```text
refinedとは
refinedはRefinement Type(篩型)をScalaで実現するためのライブラリで、既存の型に対して型レベルで満たすべき条件を指定することで、取りうる値を制限することができます。もともとはHaskellの同名のライブラリを移植したもののようです
```

__Scala__で__*Refinement Type*__を扱える__*refined*ライブラリ__を使った実装例については、@wcsakuraiさんの記事がQiitaにあります。

・ [「恵比寿のおすすめランチスポットAPIをfinchで書く(scala/finch/circe/refined)」](https://qiita.com/wcsakurai/items/b6f9f1b534a6675ddeca)

__Python__でも、型アノテーションの導入（typingモジュール）や、静的な型検査を行うことができる__*[mypy](https://qiita.com/tags/mypy)*__が登場する流れを受けて、__データ型の型チェックを行う__だけでなく、__データ値の値の範囲や配列の長さ__を__型チェックの文脈で、静的にチェック__できないか、調べてみました。

その結果、__Pythonで依存型と篩型の型クラスを宣言できるようにするスクリプト__が、GitHubで公開されていました。

・ [(GitHubリポジトリ）vixrant/python-type-theory](https://github.com/vixrant/python-type-theory)

以下のstackoverflowでのやり取りから、見つけたものです。

・ [Can Python implement dependent types?](https://stackoverflow.com/questions/43292197/can-python-implement-dependent-types)

```text:
So, can we implement a type Vect, which can be used as in
```

```Python3:
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?
```

```text:
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*して、使ってみたところ、うまく動きました。

```bash:Terminal
% 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】自作モジュールへのパスの通し方」](https://qiita.com/derodero24/items/6e2d809ceb6360211bd2)

今回は、パスは通さないで進めます。

 ```bash:Terminal
 % 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で対話インタプリタ上で宣言した関数の実装を見る方法」 ](https://teratail.com/questions/124072)

それでは、冒頭のgithubリポジトリに掲げられているサンプルコードを実行して、挙動を確認します。



###__型検査テスト１（ 成功 ）__

 ```bash:Terminal
 % 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値です。

```Python3:Python3
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型のインスタンスを生成してみます。

```Python3:Python3
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]: 
```

結果は、期待した通り、次の型エラーが発生しました。

```Python3:Python3
TypeError: Value -4 does not satify refinement N
```

それでは、*N*型の型制約条件を満たす「0よりも小さい*int*型オブジェクト」である4（正の符号を持つ整数）_を渡して、N型のインスタンスを生成してみます。

```Python3:Python3
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値です。

```Python3:Python3
In [7]: @reftype
   ...: def CapitalisedName(s: str) -> bool:
   ...:    return len(s) > 0 and s[0].isupper()
   ...: 

In [8]: 
```

これで、自作クラスである*CapitalisedName*型（クラス）が定義できました。
このクラスは、__「文字数が0よりも大きくて、（なお且つ）大文字で始まる*str*型オブジェクト」__だけを持つことができます。

それでは、コンストラクタに、「小文字で始まる文字列（*str*型オブジェクト）」である__'vikrant'__を渡して、CapitalisedName型のインスタンスを生成してみます。

```Python3:Python3
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]: 
```

結果は、期待した通り、次の型エラーが発生しました。

```Python3:Python3
TypeError: Value vikrant does not satify refinement CapitalisedName
```

「大文字で始まり、文字数が0（文字）より大きい文字列（*str*型オブジェクト）」である__'Vikrant'__をコンストラクトに渡すと、
型エラーを発生させることなく、CapitalisedName型インスタンスを生成させることができます。

```Python3:Python3
In [9]:  y = CapitalisedName('Vikrant')

In [10]: print(type(y))
<class 'str'>

In [11]: print((y))
Vikrant

In [12]: 
```

###自作した型制約付きのクラスを用いて、メソッドを定義してみる

型制約を満たす値をコンストラクタに渡した場合のみ、自作クラスからインスタンスを生成することができることが分かりました。

では、次に、「取りうる値」に制約を持つ自作型クラスを、自作メソッドを定義するときに付ける型アノテーションの中で用いてみます。
今度は、*@refine*デコレータを付けます。

ここでは、githubリポジトリにあるサンプルコードを少し変えてみました。

```Python3:Python3
In [13]: @refine
    ...: def greet(name: CapitalisedName, dept: str, age: N) -> str:
    ...:     return f"{name} さんは、 {dept}に所属する {age} 歳の社員です。"
    ...: 

In [14]: 
```

メソッドが定義できました。

それでは、第１引数"name"に、*CapitalisedName*型のインスタンスを渡して、*greet*メソッドを呼び出して実行してみます。


```Python3:Python3
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*の誤字だと思われます）



```Python3:Python3
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*を定義してみます。

```Python3:Python3
In [18]: @reftype
    ...: def LengthRestrictedString(s: str) -> bool:
    ...:     return len(s) < 7 and s[0].isupper()
    ...: 

In [19]:
```

7文字を超える文字数の文字列を、定義した*LengthRestrictedString*型コンストラクタに渡してみます。
エラーが発生しました。意図した通りです。

 
 ```Python3:Python3
 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*型のインスタンスが生成できました。

 ```Python3:Python3
In [21]: new_string = LengthRestrictedString("Bad.")

In [22]: print(type(new_string))
<class 'str'>

In [23]: print(new_string)
Bad.

In [24]: 
```

###配列（List）の長さに制約を与える方法


GitHubレポジトリでは、次のサンプルコードが掲載されています。

 ```Python3:Python3
In [35]: @refine
     ...: def MinLenList(lim: N):
     ...:     @reftype
     ...:     def LenLimit(l: list) -> bool:
     ...:         return len(l) >= lim
     ...:     return LenLimit
     ...: 

In [36]: 
```

 ```Python3:Python3
In [37]: test_list
Out[38]: ['a', 'abc', 'd']

```

*MinLenList()*メソッドに3を与えて、要素数が３以上のリストかどうかを検査するメソッド（返り値はbool型）を定義します。

 ```Python3:Python3
In [39]: lengh_condiiton_checker_func = MinLenList(3)

In [40]: print(type(lengh_condiiton_checker_func))
<class 'function'>

```

次に、配列オブジェクト*test_list*を与えてみます。

 ```Python3:Python3
In [41]: result = lengh_condiiton_checker_func(test_list)

In [42]: print(result)
['a', 'abc', 'd']

```

*test_list*は、要素数が３つで、__MinLenList(3)型の型制約を満たす__ので、__MinLenList(3)型のインスタンスの生成に成功__しました。

次に、要素数が3より少ない配列を与えてみます。

 ```Python3:Python3
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]: 
```

意図した通り、エラーが発生しました。

配列の要素がすべて同じデータ型であるという制約は与えていないので、要素数が３個以上の配列でありさえすれば、型制約は満たします。

 ```Python3:Python3
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*型クラスのインスタンスを受け取るよう定義しました。

 ```Python3:Python3
 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引数に渡してみます。

 ```Python3:Python3
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*型クラスの値制約を満たすため、今度は実行に成功しました。

___


###配列の長さ（要素数）に制約を与える：失敗コード事例
以下は実行エラーになった。

```Python3:Python3
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]: 
```

#####以下もエラー

 ```Python3:Python3
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]:
```


 ```Python3:Python3
 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]: 
```