単一化
2つの項が同一または同等であるかどうかを判定する
同一を示すものを統語論的単一化
同等を示すものを意味論的単一化
と呼ぶ
「同等であるかどうか」は換言すれば「適当な具体型を代入したときに一致することがあるかどうか」
型推論の文脈では
2つの型を引数にとって、それらが等しいかどうかを判定する
hsunify :: Constraint -> Constraint -> TI BoolunyfyVarは何をしているのか
片方が型変数で、片方が具体型の場合に実行する
例
例
| 入力1 | 入力2 | 結果 |
| CVar 1 | CInt | True |
| CInt | CBool | False |
| CVar 1 | CVar 2 | True |
| CLambda (CVar 1) (CVar 2) | CLambda (CVar 2) (CVar 3) | True |
| CVar 1 | CLambda (CVar 2) (CVar 1) | occurs checkによりFalse |
関連
変数が片方にしか存在しない単一化と見ることができる
参考