Haskell 型別變數是隱式量化的。關鍵字forall出現在 之后::。
例如，const型別簽名
const :: a -> b -> a
寫成：
const :: forall a b. a -> b -> a
我的問題是：我怎樣才能有效地推斷簽名
const :: forall a. a -> a -> a
從那個定義。我嘗試使用從一階邏輯中學到的概念，例如普遍排除法，但無法從理論的角度證明這一點。
當然，這是有道理的，因為沒有什么可以排除b與a.
為什么我不能證明使用該推理規則是合理的？因為我不能在第二個量詞上使用消除，因為變數會發生沖突。我無法b用a.
uj5u.com熱心網友回復：
考慮：
(1) const :: forall a b. a -> b -> a
(2) const :: forall a. a -> a -> a
你不能從（1）推斷（2）；如果可以的話，這意味著它const 總是有一個型別擬合forall a. a -> a -> a（并且在（1）中并不明顯，因為我們還沒有應用足夠的推理步驟）。但我顯然可以在where has type之類const的情況下使用。const True 'a'constBool -> Char -> Bool
您可以做的是意識到 (2) 是 (1) 的實體化。b與a 一般情況不同，但是（如您所說）沒有什么可以阻止與任何一種特定用法b相同的事物。a因此，從使用的背景關系中，const您可能能夠推斷出特定用法具有 type forall a. a -> a -> a。例如，這發生在：
silly :: forall a. a -> a
silly x = const x x
您也可以const :: forall a b. a -> b -> a單獨判斷，如果您選擇實體化與您得到b的相同。我們總是將其作為一個選項，因為該型別承諾對所有可能的型別都有效，其中包括我們總是選擇相同事物的可能性子集。aconst :: forall a -> a -> abba
為此，我們只需將bs替換為as（在我們實體化的量詞的范圍內，但這就是整個運算式）。您表示懷疑您是否可以這樣做，因為變數會發生沖突，但是將一個變數實體化為與另一個變數相同是我們在這里所做的重點。這與簡單地重命名變數并通過給變數賦予本應不同的相同名稱而意外更改運算式不同；在這里，我們故意選擇檢查不明顯的特殊情況。
但是沒有從const :: forall a -> b -> a單獨（沒有任何使用它的背景關系）到的純推理鏈const :: forall a. a -> a -> a，因為當您進行更改時，您正在削弱/專業化const；您選擇將其限制為最通用型別的子型別。b如果不添加您選擇限制為與 相同的附加資訊，推理規則不會讓您從 (1) 到 (2) a。（在 Haskelly 術語中，這將是一個額外的a ~ b約束）
轉載請註明出處，本文鏈接：https://www.uj5u.com/houduan/493300.html