第６回

課題４

・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

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

   1 let f f = f f;;

課題５とか

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

• generalize
  • 日本語にすると「一般化」というところでしょうか？
  • 型tから型スキーマ∀P.tを生成します。
  • Pは型変数の集合で、tに含まれる型変数のうち多相的に扱うものからなります。
  • 具体的なPの決め方は(tに含まれる型変数の集合)-(型環境に現れる型変数の集合)
  • 「型環境に現れる型変数」というのは、例えば型環境にx, yという二つの変数（型変数ではない）が登録されていたとき「(xの型に含まれる型変数の集合)∪(yの型に含まれる型変数の集合)」がそれにあたります。

  • 例えば、「a->b」という型があって、型変数bだけが型環境にすでに現れている場合、この型をgeneralizeすると「∀{a}.a->b」という型スキーマが返されます。

• instantiate
  • 日本語で「実体化」。本によってはspecializeという名前だったりするようです。
  • 型に含まれる型変数を型スキーマの情報にしたがって新しい型変数で置き換えます。

  • 例えば、「∀{a}.a->b」という型スキーマがあったら、a->bという関数型のaという型変数をnew_typ_var()などで作った新しい型変数（cとします）でおきかえて、c->bという型を返します。

• get_typ_vars
  • 型に含まれる型変数の集合を返します。

  • 例えば、「((a * int) * (b * bool)) list -> (a * b) list」のような型をget_typ_varsに入れたら{a, b}という集合が返ってきます。

  • リストやタプル、関数型などを処理しようとすると難しいかも知れませんが、再帰を使うとうまく書けるかもしれません。

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

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

課題８以降

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

• 課題8（多分9, 10も）の基本的なアイディアは、(fun x -> …)というfun式の引数xをlet式と同様に多相型として扱うこと。

• ただ、本当に多相型として扱ってしまうと、インタープリタが止まらなくなる場合がある。
• 例えば、

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

• この辺りの問題をいい感じに解決するようにがんばる。
• 課題11は、綺麗に解けたら論文が書けるレベル。
• 汚い解法ならいくつかある。
• 最低の方法としては、parser.mlyをいじって、問題にあるような式を特別にパースして処理すること。
• でももうちょい綺麗な方法で実装してほしいらしい。

Categoryノート