ランク１多相の続き

何度も言及してすみません。いや、本当に…（笑）

http://d.hatena.ne.jp/succeed/20061030#1162196029

一瞬、僕も悩みましたが、polymorphic recursionがない、ということのようです。これは普通のMLでも同様ですが、Ｏ堀先生のランク１多相でも、（大ざっぱに言うと）let rec x = eの型推論をするときは、eの中ではxは単相的として（どこにも）∀をつけず、後からxの型（の先頭）に∀を追加する、ということだそうです。通常のMLでも、polymorphic recursionを許すと型推論が決定不能になることが知られています（関連スレッド…になっていませんが）。

問題を誤解していたらご容赦。