続・ポイントフリー的ななにか
OCamlのlet多相は、
- 値は多相で処理。それ以外は単相。
- 単相が多相の部分型になってるときは、多相を回復。
という二段階。で、この部分型判定には、単相型がcovariantな位置にのみ出現するかどうかを調べる。covariantな位置というのは、要するに関数型の右側のこと。[追記]もうちょっと正確に言うと、型の大小関係(部分型の関係)を保存する演算の事をcovariantな演算と言い、多相を回復したいと思っている型が、単相型変数へのcovariantな演算のみで構成されていれば、多相への部分型が成立するので回復させるぜ!という事。
さて、これだけの原理に乗っ取って実例を確認してみましょう。
# let x = ([], ());; (* 右辺が値なので多相ですね *) val x : 'a list * unit = ([], ()) # let x = fst ([], ());; (* 右辺が値じゃないけど多相! 部分型だからね! *) val x : 'a list = [] # let x = fun x -> List.map (fun x -> x) x;; (* これも右辺が値なので多相. *) val x : 'a list -> 'a list = <fun> # let x = List.map (fun x -> x);; (* おっと、型変数が左側に出てきたので多相が回復できない! *) val x : '_a list -> '_a list = <fun>
(注)http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdfの受け売りなので、ぜひ原典を参照されたし。