|
141
|
1 -title: unification
|
|
|
2
|
|
|
3 Unification (単一化) は、二つの項が同じになる可能性があるかどうかを調べる。
|
|
|
4
|
|
|
5 これは、引数に data 型がある時にも起きる。
|
|
|
6
|
|
|
7 可能性がなければ失敗する。
|
|
|
8
|
|
|
9 ---Term
|
|
|
10
|
|
|
11 Term は以下の規則によって型と一緒に構築される。
|
|
|
12
|
|
|
13 1. Haskell の変数 x,y,z は項。つまり let a = ... で宣言された小文字で始まる記号。対応する型(変数で指定された)を持つ。
|
|
|
14 1 や 'a' も対応する型を持つ項である。
|
|
|
15
|
|
|
16 2. u が型U、v が型V を持てば、(u,v) は型(U,V)を持つ項である。
|
|
|
17
|
|
|
18 3. 型(U,V)を持つ項 t に対して、fst t は型U を持つ項、snd t は型 V を持つ項である。
|
|
|
19
|
|
|
20 4. v が型V を持つ項で、x0,x1,...,xn が型Uを持てば、 \x0 x1 ..., xn -> v は項である。
|
|
|
21 Haskell によって変数の名前のスコープは適切に扱われるとする。
|
|
|
22
|
|
|
23 5. t が型 U->V を持ち、u が 型U を持てば、 t u は型V を持つ項である。
|
|
|
24
|
|
|
25 --単一化
|
|
|
26
|
|
|
27
|
