Haskell存在量化的詳細信息

我對存在量化的類型是什麼以及可以在哪裏使用有一個大致的瞭解。但是，從我迄今爲止的經驗來看，爲了有效地使用這個概念，需要了解許多警告。Haskell存在量化的詳細信息

問題：有沒有什麼好的資源可以解釋GHC中如何實現存在量化？即

如何統一存在類型的工作 - 什麼是可以統一的，什麼是不可以的？
按什麼順序對類型進行後續操作？

我的目標是更好地理解GHC向我發出的錯誤消息。消息通常沿線"this type using forall and this other type don't match"說，但是他們沒有解釋爲什麼是這樣。

2012-02-13 julkiewicz

Simon Peyton-Jones的論文報道了細節的細節，儘管需要大量的技術專業知識才能理解它們。如果你想讀一篇關於Haskell類型推斷如何工作的論文，你應該閱讀一下廣義代數數據類型（GADTs），它將存在類型和其他幾個特徵結合在一起。我在http://research.microsoft.com/en-us/people/simonpj/的論文列表中建議「GADT的完整和可確定的類型推斷」。

存在量化實際上很像普遍量化。這裏舉一個例子來突出兩者之間的相似之處。功能useExis是無用的，但它仍然是有效的代碼。

data Univ a = Univ a 
data Exis = forall a. Exis a 

toUniv :: a -> Univ a 
toUniv = Univ 

toExis :: a -> Exis 
toExis = Exis 

useUniv :: (a -> b) -> Univ a -> b 
useUniv f (Univ x) = f x 

useExis :: (forall a. a -> b) -> Exis -> b 
useExis f (Exis x) = f x

首先，請注意toUniv和toExis幾乎相同。它們都有一個自由類型參數a，因爲這兩個數據構造函數都是多態的。但a出現在toUniv的返回類型中，但它不出現在toExis的返回類型中。當涉及到使用數據構造函數時可能遇到的那種類型錯誤時，存在類型和通用類型之間沒有太大區別。

二，請注意排名第二的forall a. a -> buseExis。這是類型推斷中的重大差異。從模式匹配(Exis x)中獲得的存在類型就像一個傳遞給函數體的額外的隱藏類型變量，它不能與其他類型統一。爲了使這個更清楚，下面是最後兩個函數的一些錯誤聲明，我們試圖統一不應該統一的類型。在這兩種情況下，我們強制將x的類型與不相關的類型變量統一起來。在useUniv中，類型變量是函數類型的一部分。在useExis中，它是來自數據結構的存在類型。

useUniv' :: forall a b c. (c -> b) -> Univ a -> b 
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c' 
          -- Variable 'a' is there in the function type 

useExis' :: forall b c. (c -> b) -> Exis -> b 
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'. 
          -- Variable 'a' comes from the pattern "Exis x", 
          -- via the existential in "data Exis = forall a. Exis a".

來源

2012-02-13 16:39:49 Heatsink

Haskell存在量化的詳細信息

回答

相關問題