爲什麼'id id`不是OCaml中的值？

Question

我仍在嘗試瞭解OCaml中的值限制，並通過Wright's paper進行了解讀。並且在其中，(fun x -> x) (fun y -> y)不是一個語法值，它也表示lambda表達式應該是一個值。我在這裏有點困惑，是不是id id其本質上也是lambda表達式？在OCaml中真正算作語法值的是什麼？

我也試圖在utop，發現這些：

utop # let x = let x = (fun y -> y) (fun z -> z) in x ;; 
val x : '_a -> '_a = <fun> 

這裏id id不是一個價值，它無法逃避的價值限制，但

utop # let x a = let x = (fun y -> y) a in x ;; 
val x : 'a -> 'a = <fun> 

這裏id a似乎被視爲值。

它們都是功能應用，有什麼區別？

Answer 1

因此，這裏涉及兩個概念：let-polymoprhism和價值限制。讓 - 多態性不允許所有非限制值的類型泛化。或者，在不使用雙重否定的情況下，只有在引入了let-binding的情況下，才允許值爲多態。這是一種過度逼近，即它可能不允許有效的程序（有誤報），但它永遠不會允許一個無效的程序（它將保持健全性）。

價值限制是另一個過度逼近，這是必要的，以保持命令式程序的健全性。它不允許非語法值的多態。 OCaml使用這種過度逼近的更精確版本，稱爲relaxed value restriction（實際上允許某些非語法值是多態的）。

不過，讓我先解釋一下什麼是語法值：

通俗地說，句法值是可以不用做任何的計算來計算的表達式，例如，請考慮下面就讓結合：

let f = g x 

這裏f不是一個語法值，因爲爲了獲得需要計算表達式g x的值。但是，在下面，

let f x = g x 

值f是語法，它會更明顯，如果我們將刪除糖：

let f = fun x -> g x 

現在很明顯，即f是語法，因爲它綁定到lambda表達式。

該值被稱爲句法，因爲它是直接在程序中定義的（在語法中）。基本上，它是一個可以在靜態時間計算的常數值。略更正式，以下值被認爲是語法：

• 常數（即，像整數和浮點文本）
• 構造函數，只有包含其他簡單的值
• 函數聲明，即表達式樂趣或功能，或等效讓結合開始，let f x = ...
• 形式的let綁定讓VAR =表達式1在表達式2，其中兩個表達式1和表達式2是簡單值

現在，當我們非常確定什麼是語法的時候，讓我們更仔細地看看你的例子。讓我們從賴特的例子開始，實際上是：

let f = (fun x => x) (fun y => y) 

，或者通過引入let id = fun x -> x

let f = id id 

您可能會看到，那f這裏不是語法值，雖然id是語法。但爲了得到f的值，你需要計算 - 所以這個值是在運行時定義的，而不是在編譯時。

現在，讓我們desugar你的例子：

let x a = let x = (fun y -> y) a in x 
==> 
let x = fun a -> let x = (fun y -> y) a in x 

我們可以看到，x是句法值，因爲左邊是一個lambda表達式。拉姆達表達式的類型是'a -> 'a。你可能會問，爲什麼表達式的類型不是'_a -> '_a。這是因爲值限制只在頂層引入，並且lambda表達式還不是一個值，它是一個表達式。從外行的角度來說，首先，最普遍的Hindley-Milner類型是根據假設推斷的，即沒有副作用，然後通過（放鬆）的價值限制來減弱推斷類型。類型推斷的範圍是一個let綁定。

這就是所有的理論，有時它不是很明顯，爲什麼一些表達式是很好的類型，而具有相同語義但寫法稍有不同的表達式沒有很好的類型。直覺可能會說，這裏有什麼問題。是的，事實上，let f = id id是一個結構良好的程序，被類型檢測程序拒絕，並且這是過度近似的示例。如果我們將這個程序轉換爲let f x = id id x，它會突然變成一個具有通用類型的良好類型的程序，儘管轉換不會改變語義（並且這兩個程序實際上編譯爲相同的機器代碼）。這是一個類型系統的侷限性，它是簡單性和精確性之間的妥協（穩健性不能成爲妥協的一部分 - 類型檢測器必須是合理的）。所以，從後一個例子總是安全的理論來看，這完全不明顯。只是爲了實驗的緣故，讓我們嘗試用你的榜樣玩，並試圖打破程序：

# let x = fun a -> let z = ref None in let x = (fun y -> z := Some y; y) a in x ;; 
val x : 'a -> 'a = <fun> 

因此，我們增加了一個參考z這裏，我們正在嘗試存儲的價值，所以，根據不同的應用程序不同的類型，我們應該能夠存儲到不同類型的相同參考值。但是，這是完全不可能的，因爲因爲x是一個語法值，所以保證每個類型x k被調用一個新的引用被創建，並且這個引用永遠不會泄漏let-definition的範圍。希望，這有助於:)

Answer 2

這是一個應用程序，而不是一個lambda表達式。左表達式是一個函數，右表達式是該函數應用的值。

值的概念（在價值限制的意義上）是一個句法的概念。這不是關於價值的類型。