osiire’s blog

ふしぎなそふとやさん

続・ポイントフリー的ななにか

OCamlのlet多相は、

  1. 値は多相で処理。それ以外は単相。
  2. 単相が多相の部分型になってるときは、多相を回復。

という二段階。で、この部分型判定には、単相型が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の受け売りなので、ぜひ原典を参照されたし。