爲什麼OCaml使用多態變體的子類型？

Question

我剛剛閱讀了關於row polymorphism以及它如何用於可擴展記錄和多態變體。

但是，Ocaml使用子類型爲多態變體。爲什麼？它比行多態性更強大嗎？

Answer 1

爲了補充Gabriel的答案，一個方法來思考這是一個亞型同時提供普遍和存在多態性的弱勢形態。當參數多態性的兩個方向都可用時，則子類型的表達性大部分被包含在內（特別是當沒有深度子類型時）。但Ocaml並非如此。

Ocaml通過實際的通用多態性取代了通用方面，但保留了子類型以爲您提供一種存在量化的形式，否則它將不具備。這需要形成例如異構集合，例如<a: int> list，其中您希望能夠存儲任意對象，該對象至少具有正確類型的a方法。

我會更進一步說，雖然這通常被解釋爲Ocaml世界中的子類型，但您實際上可以將封閉行解釋爲在（未知）尾部上存在量化的。然後通過:>進行強制導入，從而更加忠實於行構建的參數多態的世界。 （當然，根據這個解釋，#會做隱式的存在性消除。）如果我要從頭開始設計一個類似Ocaml的系統，我可能會嘗試以這種方式對它進行建模。

Answer 2

OCaml使用都行polypoprhism和分型爲多態變體（和對象，就此而言）。 「開放」對象類型< 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 ]之間進行投射。

行多態性允許避免需要有限的量化來表達類型，例如「採用至少具有方法m的對象並返回相同類型的對象」：因此子類型相當簡單，明確，並且不能被抽象出來。相反，行多態性更容易推斷，並且對類型系統的其餘部分會更好。使用封閉類型和明確的子類型應該很少有必要，但偶爾也很方便 - 特別是保持類型關閉會產生更容易理解的錯誤消息。