卒論で死にそうです。色々。
PPLのポスター発表に間に合うのでしょうか、その前に卒論発表会に間に合うのか…。
それはさておき、型注釈を色々見ていたら、MLも闇だなぁと思ってたのでちょっとメモしてみます。
追記の追記の追記：
@camloebaさんにツッコミをいただきました。型注釈という言葉は不適切ということでした。
毎度ありがとうございます[´･_･`]
@no_maddo 型注釈とは言わない。型制限と言う
— 星のキャミバ様 (@camloeba) 2014, 2月 17@no_maddo Parenthesized expressions can contain a type constraint, as in ( expr : typexpr ). それを type annotation と呼ぶところから間違いが始まります
— 星のキャミバ様 (@camloeba) 2014, 2月 17
http://caml.inria.fr/pub/docs/manual-ocaml-4.00/expr.html
をよんでも確かにtype annotationという言葉は使われてないですね。ありがとうございます！！！
例題はこちら。
言われてみればまぁ通らないよねって感じです。
追記：
何も通らない理由を書いてなかったので、勿論MLに親しんでいる諸兄らは問題なく理解されると思いますが、一応理由を追記しておきます。
型変数のスコープの問題です。ちゃんとしたテクニカルな説明はちょっと難しいので、自分の理解を書いておきます。
上の通らない例で、'aのスコープはｆの定義が始まって終わるまでです。
なので、fの中でｇが使われるとき、まだ'aの型推論は終わっていません。なのでｇは多相関数にはなりません。
MLの型推論は大雑把に言って、型の制約に関する方程式を解いて、残った型変数に（制約がないもの）にforallをつける、というものです。
推論が行われている最中では、関数は単相的であるとして扱われます。なぜならばpolymorphic recursionは許されていないからです。
（なぜ許されないかというと、これを許すと型が決定不能になるからです。なぜ型が決定不能になるかは論文を読んでください…。）
というわけで、上の例ではｇの型について推論が終わっていない段階で多相的に扱おうとしているため、エラーが発生するのです。
（追記ここまで）
追記の追記：
もしかしたらちょっとした落とし穴になるんじゃないかな？と思いました。
let (g:'a) なんてわざとらしいですが、例えばこれがlet (g:'a -> 'a)と書くのはありえそうじゃないですか？
あまりしそうにないですが、ないことはないだろうなぁと思いました。
はて、世の中のOCamlの解説している文献に、型変数のスコープのことは書いてあったかしら…。
（追記の追記おわり）
ちょっと卒論と関わるので調べていました。
それ以外にもOCamlのソースコード読んでると、副作用バリバリだったりtypedtreeの構造がこうなっているーとか面白いこといっぱいあるのですが、今回はこれくらいで。
あ、これは紹介します。ちょっと前に教えてもらったものですが、
How OCaml type checker works -- or what polymorphism and garbage collection have in common
http://okmij.org/ftp/ML/generalization.html
