行ポリモーフィズムと、それを拡張可能なレコードとポリモーフィック バリアントに使用する方法について読みました。
ただし、Ocaml は多相バリアントのサブタイピングを使用します。なんで？行ポリモーフィズムよりも強力ですか?
質問する
2108 次
2 に答える
13
OCamlは行多形性と多形バリアント (さらに言えばオブジェクト) のサブタイピングの両方を使用します。行ポリモーフィズムは、「オープン」オブジェクト型< m1 : t1; m2 : t2; .. >(..文字どおり型の一部)、または「オープン」バリアント型に関係します[> `K1 of t1 | `K2 of t2 ]。サブタイピングは、閉じた非ポリモーフィック型<m1:t1; m2:t2> :> <m1:t1> または間でキャストできるようにするために使用されます[ `K1 of t1 ] :> [ `K1 of t1 | `K2 of t2 ]。
行ポリモーフィズムにより、「少なくとも method を持つオブジェクトを取得しm、同じ型のオブジェクトを返す」などの型を表現するための制限された量化の必要性を回避できます。したがって、サブタイピングはかなり単純で明示的であり、抽象化することはできません。それどころか、行ポリモーフィズムは推論が容易であり、型システムの残りの部分とうまく連携します。閉じた型と明示的なサブタイプを使用する必要はほとんどありませんが、便利な場合もあります。特に、型を閉じたままにしておくと、理解しやすいエラー メッセージが生成される可能性があります。
于 2013-05-27T15:02:30.923 に答える
8
ガブリエルの答えを補完するために、これについて考える 1 つの方法は、サブタイプ化が普遍的および実存的ポリモーフィズムの両方の弱い形式を提供することです。パラメトリック ポリモーフィズムの両方の方向が利用可能な場合、サブタイピングの表現力はほとんど考慮されます (特に深度サブタイピングがない場合)。しかし、Ocaml ではそうではありません。
Ocaml は普遍的な側面を実際の普遍的なポリモーフィズムに置き換えますが、サブタイピングを続けて、そうでなければ存在しない形式の存在量化を提供します。これは、たとえば、少なくとも正しいタイプ<a: int> listのメソッドを持つ任意のオブジェクトを格納できるようにするなど、異種コレクションを形成するために必要です。a
これは通常、Ocaml の世界ではサブタイピングとして説明されますが、実際には閉じた行を (未知の) テールで存在量化されたものとして解釈することができます。その場合、強制による:>導入は実存的な導入となり、それによって、行が構築されるパラメトリック ポリモーフィズムの世界により忠実なままになります。(もちろん、この解釈の下では、#暗黙の存在排除が行われます。) Ocaml のようなシステムをゼロから設計する場合、おそらくそのようにモデル化しようとするでしょう。
于 2013-05-27T15:33:29.703 に答える