第6回

課題4

・type_check_exprの作り方

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

たとえば推論規則

Γ├e_1:t_1,C_1

Γ├e_2:t_2,C_2

Γ├e_1 aop e_2:int,{t_1=int}∪{t_2=int}∪C_1∪C_2

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

(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

kd先生が発見なさったコーナーケース。これは型エラーになるはず。-- furaga

   1 let f f = f f;;

課題5とか

・レジュメで言われてる各関数が何をするかが自明でない気がするので、メモっておきます。-- furaga

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

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

>> let f x = x in f f;;
- : 'a -> 'a = <fun>
>> 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>

課題8以降

さる御方から得た情報を書いておきます。-- furaga

let fix f = (fun x -> f x x) (fun x -> f x x);;


Categoryノート

関数・論理型プログラミング実験/課題メモ/第6回 (最終更新日時 2011-06-11 01:45:35 更新者 furaga)