OCaml函數的多態變體不夠多態嗎？

OCaml給出function `A -> 1 | _ -> 0類型[> `A] -> int，但爲什麼不是[> ] -> int？OCaml函數的多態變體不夠多態嗎？

這是我的推理：

function `B -> 0具有類型[<`B] -> int。添加一個`A -> 0分支，使其function `A -> 1 | `B -> 0鬆開到[<`A|`B] -> int。該函數在它可以接受的參數類型中變得更寬容。這是有道理的。
function _ -> 0有型號'a -> int。這種類型可以與[> ] -> int一致，而[> ]是一個已經開放的類型（非常寬容）。添加`A -> 0分支使其function `A -> 1 | _ -> 0限制的類型爲[>`A] -> int。這對我來說沒有意義。事實上，增加另一個分支`C -> 1將使它[>`A|`C] -> int，進一步限制類型。爲什麼？

注：我不是在尋找解決方法，我只是想知道這種行爲背後的邏輯。

在相關說明中，function `A -> `A | x -> x的類型爲([>`A] as 'a) -> 'a，雖然這也是該參數的限制性開放類型，但我可以理解其原因。該類型應與'a -> 'a,[>` ] -> 'b,'c -> [>`A];唯一的做法似乎是([>`A] as 'a) -> 'a。

它對我的第一個例子是否存在類似的原因？

來源

2012-05-26 sin3.14

一個可能的答案是，類型[> ] -> int將允許參數(`A 3)但這不允許爲function `A -> 1 | _ -> 0。換句話說，該類型需要記錄`A不帶參數的事實。

來源

2012-05-26 19:31:03

很好的理由，謝謝。但是作爲「錄製」的副作用，這仍然會導致像「'（function'A - > 1 | _ - > 0）」（（fun x - >（match B with'B - >（）） ; x）'B）''無法進行類型檢查。可能有更深的原因？在接受你的答案之前，我會再等一等。 –

你會提出什麼類型的'函數'A k - > k | _ - > 0''？ –

gariguejej回答如下。 –

如Jeffrey所解釋的，(function `A -> 1 | _ -> 0)的分型是合理的。

(function `A -> 1 | _ -> 0) ((fun x -> (match x with `B ->()); x) `B)

未能進行類型檢查，在我看來應該解釋爲表達式的後半部分。事實上，功能(fun x -> (match x with `B ->()); x)的輸入類型爲[< `B]，而其參數`B的類型爲[> `B ]。兩種類型的統一給出了封閉類型[ `B ]，其是而不是多態。它不能與從(function `A -> 1 | _ -> 0)獲得的輸入類型[> `A ]統一。

幸運的是，多態變體不僅依賴於（行）多態性。您還可以在需要放大封閉類型的情況下使用子類型：[ `B ]是子類型，例如[`A | `B]，它是[> `A ]的實例。子類型轉換在OCaml中使用語法(expr :> ty)（轉換爲某種類型）或(expr : ty :> ty)在OCaml中爲顯式，或者在不能推斷域類型正確的情況下爲(expr : ty :> ty)。

你可以寫，因此：

let b = (fun x -> (match x with `B ->()); x) `B in 
(function `A -> 1 | _ -> 0) (b :> [ `A | `B ])

這是良好的類型。

來源

2012-05-27 06:34:30 gasche

是的，我知道，並且我正是用這個例子來形成的。在我看來，問題在於''''''A'''太過限制了，不如人們所希望的。但是好的，由於無法表達''[]]約束'A不需要參數''，所以我們無能爲力。 –

的原因是一個非常實用的一個：
在老版本的OCaml的推斷類型是

[`A | .. ] -> int

這意味着一個沒有參數，但可以不存在。

然而這種類型是unifiable與

[`B |`C ] -> int

這導致`阿被丟棄，沒有任何形式的檢查。

它容易引入錯誤拼寫錯誤。
因此，變體構造函數必須出現在上限或下限中。

來源

2012-05-28 13:30:00 gariguejej

謝謝你的完整答案。不幸的是我沒有投票的聲望。 –

哦，你是Jacques Garrigue。保持良好的工作！只是告訴你，在閱讀OCaml手冊時，我想到了這個問題，「提前使用」一節。這個問題的一個複雜的例子出現在那裏，不是。我在某個地方看過一個博客，稱這個手冊爲「一個主要問題」，所以我只是想問一下。 –

OCaml函數的多態變體不夠多態嗎？

回答

相關問題