let rec の型推論と多相型

K. Sakaguchi @pi8027

やっぱり specialize 挟んでも推論一発で終わるっていうのは嘘な気がするし、自前の推論器で型がおかしくなるケースは作れた。@mayahjp さんを質問攻めにする会が必要!

mayah@節電中 @mayahjp_old

@pi8027 それ自分が考えているのより強い型推論じゃないかなー、というわけで例を下さい。

K. Sakaguchi @pi8027

@mayahjp https://gist.github.com/702923 こういうのです。

K. Sakaguchi @pi8027

しかしこれくらい推論してくれないと困る……。

mayah@節電中 @mayahjp_old

@pi8027 これぐらい何の問題もなく推論できると思うんですけど、どういう結果がでてるんでしょう。というか github から source 落としてきて走らせればいいのか

K. Sakaguchi @pi8027

@mayahjp 上から調べていくので、下に定義のある名前の型を取ってこれないのです。もし上手く順序を入れ替えたとしても、一部の再帰関数などで同じ現象が起きる気がします。

日比野 啓 (Kei Hibino) @khibino

@pi8027 @mayahjp 構文解釈木の任意の部分式の型をunifyで特殊化していくんだよね? < 上から調べていくので、下に定義のある名前の型を取ってこれないのです。

日比野 啓 (Kei Hibino) @khibino

@pi8027 @mayahjp でもlet多相にしたかったら、その操作の前に letを展開する操作が必要なんじゃないかな

日比野 啓 (Kei Hibino) @khibino

@pi8027 @mayahjp ところでgistにあるコードの # は case ... of と思えば良い?

日比野 啓 (Kei Hibino) @khibino

@pi8027 @mayahjp unifyの操作は再帰で一発なんじゃないかと

日比野 啓 (Kei Hibino) @khibino

@pi8027 @mayahjp 構文解釈木に対する再帰で。

日比野 啓 (Kei Hibino) @khibino

@pi8027 @mayahjp とここまで書いて、letrec の多相はどうやるんだかちゃんと分かっていないことに気がついた

Jun Furuse @camlspotter

fresh な型変数aを与えておいて、bodyを推論し、単一化終わった後のS(a)をgeneralizeする。 RT @khibino: @pi8027 @mayahjp とここまで書いて、letrec の多相はどうやるんだかちゃんと分かっていないことに気がついた

日比野 啓 (Kei Hibino) @khibino

おお、ありがとうございます。< @camlspotter fresh な型変数aを与えておいて、bodyを推論し、単一化終わった後のS(a)をgeneralizeする。RT @khibino: @pi8027 @mayahjp .. letrec の多相はどうやるんだか ..

Jun Furuse @camlspotter

副作用があるとS(a)の計算が要らなくて超クールなのですが。cf ocaml RT @khibino: おお、ありがとうございます。< @camlspotter fresh な型変数aを与えておいて、bodyを推論し、単一化終わった後のS(a)をgeneralizeする。

日比野 啓 (Kei Hibino) @khibino

unifyを型変数への代入で、ということですよね。初めて見たときはちょっと感動しました RT @camlspotter 副作用があるとS(a)の計算が要らなくて超クールなのですが。cf ocaml RT @khibino: おお、ありがとうございます。

Jun Furuse @camlspotter

pure ではそのへんをどう頑張るか、なんか研究あったと思いますが、わざわざ自縛したうえでの競争なんで興味が持てず。まあ普通でいいんじゃん、はじめは。 RT @khibino: unifyを型変数への代入で、ということですよね。初めて見たときはちょっと感動しました

Jun Furuse @camlspotter

ごめん、body は definition ね。in の後の式じゃないよ。 RT @camlspotter: fresh な型変数aを与えておいて、bodyを推論し、単一化終わった後のS(a)をgeneralizeする。

日比野 啓 (Kei Hibino) @khibino

了解です RT @camlspotter ごめん、body は definition ね。in の後の式じゃないよ。 RT @camlspotter: fresh な型変数aを与えておいて、bodyを推論し、単一化終わった後のS(a)をgeneralizeする。

mayah@節電中 @mayahjp_old

@khibino @camlspotter @pi8027 おっと、みていない間にこんなに。let rec はそれでいいんですが、let rec id x = x and hoge () = id 1 みたいにすると、id は int -> int と推論されてしまう。

mayah@節電中 @mayahjp_old

@khibino @camlspotter @pi8027 で、@pi8027 さんのやつは let rec でつなぐと id の型が残念になってしまうので (多相型じゃなくなる)、ちょっと違うことをやらないといけない。まあ単純に Haskell の型推論なんですが。

mayah@節電中 @mayahjp_old

この場合どうすんだっけ、あとで制約条件とくのなら簡単なんだが Haskell はどうやって実装してるんだっけな

mayah@節電中 @mayahjp_old

GHC でやったらやっぱちゃんと id の型は t -> t なので、let rec みたいなことにはならない。

おしいれのぼうけん @osiire

こういうことですね。 # let rec id : 'a. 'a -> 'a = fun x -> x and hoge () = id 1;; val id : 'a -> 'a = <fun> val hoge : unit -> int = <fun>

日比野 啓 (Kei Hibino) @khibino

うーん、OCamlと同じやりかたでは多相にできないんですね ... @osiire @mayahjp @khibino @camlspotter @pi8027