第６回

課題４

・type_check_exprの作り方

まあ実装ゲーです。レジュメの最後に載っている推論規則をコードに直せば終わり。（タプル・リストに対応させようと思ったら自分で考えるしかないですが）

たとえば推論規則

をコードに直すには、この推論規則を次のように読みます。

(1)式e_1を型推論した結果導出された型と制約を(t_1,C_1)とし、

(2)式e_2を型推論した結果導出された型と制約を(t_2,C_2)とすると、

(3)式「e_1 aop e_2」の型は「int」で、制約は「{t_1=int}∪{t_2=int}∪C_1∪C_2」である。

つまり、再帰的にe_1,e_2にtype_check_exprを適用した結果をlet 〜 in式で(t_1,C_1),(t_2,C_2)とおいておき（別に置かなくてもできるけど、ごちゃごちゃする）、

型、制約の組として「(int,(t_1,int)::(t_2,int)::(C_1@C_2)」を返せばいいってこと。

具体的には以下（ADD）。

   1   |ADD(e1,e2) ->
   2      let (t1,c1) = type_check_expr typeenv e1 in
   3      let (t2,c2) = type_check_expr typeenv e2 in
   4         (INT,t1::t2::(c1@c2))

まあ、SUBとかMULとかもこのパターンにORパターンでまとめて記述するといいと思うよ。-- TakuyaKuwahara

課題５とか

多相型を実装してしまった方々に対して。

筆者がハマったテストケースと（レジュメにしたがって作った場合における）正しい出力を載せておきます。--furaga

>> fun y -> let f x = y in f 0;;
- : ('a -> 'a) = <fun>
>> let rec f x = g x and g x = x;;
val g : ('a -> 'a) = <fun>
val f : ('a -> 'a) = <fun>
>> f f;;
- : ('a -> 'a) = <fun>
>> g g;;
- : ('a -> 'a) = <fun>
>> let rec f x = x and g x = f x;;
val g : ('a -> 'a) = <fun>
val f : ('a -> 'a) = <fun>
>> f f;;
- : ('a -> 'a) = <fun>
>> g g;;
- : ('a -> 'a) = <fun>

Categoryノート