##この記事で行うこと
要素の数が、[ある数値以上、ある数値以下]であるlist配列であること、という__型制約__を持つ__自作クラス（自作データ型）__を__Pythonで宣言__してみます。
このデータ型のインスタンスを生成するときに、__コンストラクタに、上記の条件を破る引数を与えると、TypeErrorが発生して、Pythonは処理を終了__します。
なお、__このlist配列は、任意のデータ型のインスタンスを要素に持つことができるという条件__も、おまけに付け加えてみます。
さらに、__複数の異なるデータ型のインスタンスを要素に持つことも許容__します。
__上記の条件をすべて満たすデータ型__を、Pythonで定義して、使ってみます。
（ 関連記事 ）
##（ 必要な外部資源 ）
ここでは、以下のGitHubリポジトリにあるPython用のモジュール__をgit clone__して、利用します。
・ (GitHubリポジトリ）vixrant/python-type-theory
% 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.
%
####（ 実行環境 ）
・ IPython対話型インタプリタ（Python 3.9.0）
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したモジュールを使うことができます。
##では、はじめます。
####（ 利用するモジュールのインポート ）
from typing import List, Sequence, TypeVar
from refinement import refine, reftype
T = TypeVar('T')
まず、ある条件を記述し、条件を満たしたかどうかを、boolean（bool）値で返すメソッドを定義します。
今回は、MinN( )メソッドと、MaxN( )メソッドという2つのメソッドを定義しました。
このメソッドには、@reftypeデコーダが付されています。
@reftypeデコーダを付けることで、データ型（自作クラス）が定義されます。
@reftype
def MinN(i: int) -> bool:
return i > 0
@reftype
def MaxN(i: int) -> bool:
return i > 0
出来上がるデータ型（自作クラス）は、__上記のメソッドに記述した条件式を満たす値だけを、持つことができる型__になります。
MinN型__とMaxN型__という２つのデータ型（自作クラス）は、以下の条件を満たすインスタンスのみを生成することができます。
・ 条件１. int型の値を持つこと。
・ 条件２. 0より大きい値を持つこと。
上記の２つの条件を充足することを義務付けられたデータ型（クラス）は、__依存型（Dependent Type）__と呼ばれています。
__依存型（Dependent Type）__クラスのインスタンスは、__ある定められた条件を満たすデータ値だけ__を、インスタンスとして持つことを許されます。
・ Dependent Types と Refinement Types の違い
・ 型をさらに拡張するーーRefinement Typesについて
先程も述べたように、例えばPositive-Integerであるならば、負の整数に関しては排除されるべきだろう。そのように考えるとするならば、次のような表現だってできるはずだ(以下の例は論文によるものである)
(: max : [x : Int ] [y : Int] ~>
(Refine [z : Int ]
(and (>= z x) (>= z y))))
(define (max x y) (if (> x y) x y))
このように、型に属するであろう任意の要素を取ってきて、それに当てはまるかどうかをチェックすることによって、より厳密な型によるチェックが行える。この場合であるならば、「Int型に属するx、及びyは、必ずzというより上位の数を所持している」ということになる(考えてみればわかるように、もし、xやyに、上位のzの数が存在しないと仮定すると、関数定義において、(> x y)という比較は成りたたない)
依存型__は、「項（数値など）に依存して決まる型」と、定義されています。
ここでいう「項（数値など）」__とは、そのデータ型がとりうる値を厳格に規定する__条件値__のことです。以下に例を挙げてみます。
【 インスタンスが持つことのできる値の制約条件（型制約）の例 】
- int型のデータの場合：値の数の範囲（例：「マイナス100〜プラス150」）
- str型や*List[T]*型の場合：配列の長さ（要素の数、文字数）の下限値と上限値
__依存型__という言葉は、Pythonの専門用語ではなく、関数型言語などのプログラミング言語の領域で使われている、プログラミング言語論の専門用語です。
__Idris__や__Racket（v6.11以降）__と呼ばれる__プログラミング言語__が、これらの型を宣言し、静的な型検査を行うことができる言語です。
次に、新しいメソッドを定義します。
今度は、定義するメソッドに、@refineデコーダを付けたメソッドの中で、さらに、@reftypeデコレータが付いた別のメソッドを定義します。
@refine
def ListLengthChecker(min_length: MinN, max_length: MaxN):
@reftype
def LenLimit(l: list) -> bool:
return (len(l) >= min_length) and (len(l) <= max_length)
return LenLimit
まず、内側にある*@reftype*デコレータが付いたメソッドは、__データ区間[min_length以上、max_length以下の値]という条件を満たすデータ値のみをとることが許されたデータ型__を、定義するものです。
ここで、__ListLengthChecker( )メソッドの型アノテーションを見ると、min_lengthとmin_length__は、それぞれ、MinN型とMaxN型のインスタンスを持つこと、という定義がなされています。
MinN型とMaxN型は、最初に定義された、__「0よりも大きな数値（int）を持つことだけが許容」されたデータ型__でした。
ListLengthChecker( )メソッドには、@Refineデコーダ__が付いています。
ListLengthChecker メソッドに、@Refineデコーダを付けることで__、新たに__ListLengthChecker型という新たなデータ型（クラス）が定義__されます。
Refinement Typeは、和訳では、__「篩（ふるい）型」と呼ばれています。この型は、「型がとりうる値が、述語で修飾されている型」__という説明のされ方をします。
*Wikipedia（英語）*の定義を引用してみます。
In type theory, a refinement type[1][2][3] is a type endowed with a predicate which is assumed to hold for any element of the refined type.
Refinement types can express preconditions when used as function arguments or postconditions when used as return types:
##（ 使い方 ）
以下の２つのステップを踏みます。
【 ステップ１ 】
ListLengthChecker型のコンストラクタに、2つの引数（min_length および max_length）を与えて、ListLengthChecker型のインスタンスを生成する。
【 ステップ２ 】
「ステップ１」で生成したListLengthCheckerr型のインスタンスに、任意のデータ型（T）を要素にもつ配列（Sequence）を引数に渡す。
コードで書くと、次のようになります。
temp_func = ListLengthChecker(min_length, max_length)
result = temp_func(data_list)
上記のコードを実行すると、以下の条件をすべて満たすかどうかが、上記のコードを実行する際に、自動的に型制約チェックが走ります。
・ 条件１. 引数として受け取ったMinN, MaxNは、int型の値を持つか。
・ 条件２. 引数として受け取ったMinN, MaxNは、0より大きい値を持つか。
・ 条件３. 引数として受け取った*Sequence[T]*型のインスタンス data_listの要素の数は、データ区間[min_length以上、max_length以下の値]の数値範囲の中にある値であるか。
__これら３つの型制約（条件）のうち、どれか１つでも満たされない制約があると、上記のコードは、「型制約エラー TypeError」__を吐いて、処理が止まります。
mypyは、Pythonのスクリプトファイルを外側から「型制約チェック」を行いますが、ここでは、Pythonスクリプトまたは、Pythonの対話型インタプリタで上記のコードが実行される瞬間に、コード内部で、上記の「型制約」が充足されているかどうかのチェックが走ります。
それでは、以下のコードを１つのメソッドに包んでみます。
temp_func = ListLengthChecker(min_length, max_length)
result = temp_func(data_list)
メソッド名として、list_length_checkerという名前を付けてみました。
def LengthRestrictedList(data_list : Sequence[T], min_length : int, max_length : int) -> Sequence[T]:
temp_func = ListLengthChecker(min_length, max_length)
try:
result = temp_func(data_list)
except TypeError:
error_message = "配列リストの長さが条件を満たしません。"
print(error_message)
result = []
return result
なお、引数として受け取るPythonのlist（配列）data_listの型アノテーションは、typingモジュールの*Sequence[T]*でも、*List[T]*でも、どちらでも構いません。
今回は、data_listの中身の要素は、任意のデータ型を持てるよう許容してみたいと思います。そのため、typingモジュールのジェネリクス（総称型）の「型変数」であるT を指定しています。
data_listの中身の要素を、intやstrやcallableなどの特定のデータ型のインスタンスに限定したい場合は、*List[int]やSequence[int]*などと、定義します。
def LengthRestrictedList2(data_list : List[T], min_length : int, max_length : int) -> List[T]:
temp_func = ListLengthChecker(min_length, max_length)
try:
result = temp_func(data_list)
except TypeError:
error_message = "配列リストの長さが条件を満たしません。"
print(error_message)
result = []
return result
##（ 挙動を確認 ）
以下で見るように、すべてが、意図した通りの挙動を示しました。（成功！）
result = LengthRestrictedList(["a", "b", "c", "e", "f"], 2, 7)
print(result)
# 実行結果
['a', 'b', 'c', 'e', 'f']
result = LengthRestrictedList(["a", 1, "c", "e", "f"], 2, 7)
print(result)
# 実行結果
['a', 1, 'c', 'e', 'f']
result = LengthRestrictedList(["a"], 2, 7)
# 実行結果
配列リストの長さが条件を満たしません。
result = LengthRestrictedList(["a", 1, "c", "e", "f"], 7, 10)
# 実行結果
配列リストの長さが条件を満たしません。
result = LengthRestrictedList2(["a", "b", "c", "e", "f"], 2, 7)
print(result)
# 実行結果
['a', 'b', 'c', 'e', 'f']
result = LengthRestrictedList2(["a", 1, "c", "e", "f"], 2, 7)
print(result)
# 実行結果
['a', 1, 'c', 'e', 'f']
del result
# 実行結果
result = LengthRestrictedList2(["a", "b", "c", "e", "f"], 2, 7)
print(result)
# 実行結果
['a', 'b', 'c', 'e', 'f']
result = LengthRestrictedList2(["a", 1, "c", "e", "f"], 2, 7)
# 実行結果
print(result)
['a', 1, 'c', 'e', 'f']
result = LengthRestrictedList2(["a"], 2, 7)
# 実行結果
配列リストの長さが条件を満たしません。
result = LengthRestrictedList2(["a", 1, "c", "e", "f"], 7, 10)
# 実行結果
配列リストの長さが条件を満たしません。