OCamlテクニック/let-poly

let多相には色々と種類があるので、ちと注意が必要です。

値制限のlet多相 &dagger;

参照型と型安全を両立させるため、let多相を値に制限する方法。 TAPLでも紹介されています。値制限は、かなーり厳しい。

# let fst (x, _) = x;;
val fst : 'a * 'b -> 'a = <fun>
# let v = fst ([], ());;
val v : '_a list = []
#

fst ([], ()) は値ではなく、関数適用なので、多相にはならない。

↑

OCamlのlet多相には基本的に値制限が付いています。ただし、型変数がcovariantな位置に現れる場合は、subtype関係から多相が回復します。

# let fst (x, _) = x;;
val fst : 'a * 'b -> 'a = <fun>
# let v = fst ([], ());;
val v : 'a list = []
#

covariantな位置というのは、(不正確ですが)関数の型を表す→の右側と思ってください。つまり例えば、関数の戻り値に型変数があるなら、それはcovariantな位置の型変数です。正確には圏論的に言うと(以下略

大堀先生が考案され、SML# に実装されている方法です。

[注意] Haskellのrank-n多相とかの話は、let多相の話ではなく、Universal Quantifiers (System Fとか)の話なので混同しないように。私はおもいっきり勘違いしていました(泣

covariantというのは、サブタイプという「関係」について、→という型構築子の右手側について関係を保存するという意味では(TAPLより) -- けいご? 2006-12-23 (土) 14:50:48
S<:Tのとき、T→U<:S→U、つまり→は左手についてサブタイプ関係を"逆"に保存するので"contra"variant, 一方V→S<:V→Tと、右手については"そのまま"なので"co"variant、という説明だったと思います(うろ覚え,しかも逆だった)。 -- けいご? 2006-12-23 (土) 14:59:07
つまり→は右手(戻り型)についてcovariant, 左手(引数)についてcontravariantという風。 -- けいご? 2006-12-23 (土) 15:11:52
サブタイプは配列・リストやi/o向き付けのチャネル型についても面白い話があるのですがそれはまた。 -- けいご? 2006-12-23 (土) 15:14:38
covariant,contravariantの解説ありがとうございます。wikipediaの解説もありますので、さらに詳しく知りたい人はどうぞ。 -- ogasawara? 2006-12-23 (土) 15:45:30
おおおー。ありがとうございます。 -- けいご? 2006-12-25 (月) 09:50:18