OCaml中的類型推理

我試圖圍繞OCaml的類型推斷符號包裹我的頭。OCaml中的類型推理

例如：

# let f x = x [];; 
val f : ('a list -> 'b) -> 'b = <fun>

對我來說很有意義。 val f需要一個函數x，它接受一個'a類型的列表並返回'b類型的東西。然後f返回一個'b類型，因爲它只是調用x。

但是，一旦我們得到更多的論據，我會變得更加困惑。

# let g a b c = a b c;; 
val g : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

我可以假設如果函數有參數，那麼類型推斷的第一個參數將始終是參數？如果我稱之爲b c，是（（a b）c）還是（a（b c））的順序？

# let rec h m n ls = match ls with 
    | [] -> n 
    | x::t -> h m (m n x) t;; 
val h : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun>

作爲該一個我很困惑，如何（ '一個 - >' B - > '一） - >' 一個推導。我可以看到'b列表對應於ls變量，最後'a對應於終端符號n的類型。

來源

2016-02-03 Chang Liu

我可以假設如果函數有參數，那麼類型推斷的第一個參數將始終是參數？

是的，函數類型的第一個參數是它的第一個參數的類型。

如果我打電話給bc，是（（a b）c）還是（a（b c））？

的順序是((a b) c)（你可以認爲這個簡單的方法）

至於這一次我很困惑，如何（ 'A - >' B - >「一） - > 'a得到了。我可以看到'b列表對應於ls變量，最後'a對應於終端符號n的類型。

你說得對。 ls有型號'b list和n有型號'a。

讓我們想想的m類型：

你知道n已鍵入'a，這樣你就可以得到(m n x)也已鍵入'a
你知道ls的類型爲'b list，這樣你就可以得到x有類型'b
m需要兩個參數'a和類型'b，並生成'a類型的結果。因此，m具有類型'a -> 'b -> 'a

因此，整個函數的類型是('a -> 'b -> 'a) -> 'a -> 'b list -> 'a

來源

2016-02-03 04:52:19 objmagic

太謝謝你了！這爲我清理了很多。如果您不介意回答，我只需再做一次後續處理：如果我們不知道類型推斷，只能從方程式中找出答案，該怎麼辦？你如何知道m的第二個arg a.k.a. x是'b'類型的，與'a'不一樣？ –

@ChangLiu對於像你這樣簡單的功能，你可以通過統一來推斷。以一種非常幼稚的方式，分配類型爲''''''''的''''''''''''''''''''''''''''''類型''''''''''''''''''' ，你可以爲這些變量定義方程，並求解方程以得出最基本的類型（'''''''''''''''''''''）。您可以搜索「算法W」以獲取更多關於類型推斷的信息。或者，你可以在OCaml中編程更多，這樣你就可以更快地進行推理:) – objmagic

OCaml中的類型推理

回答

相關問題