混淆了一個Haskell「生存包裝」

Question

從一個Haskell文件：

import GHC.Exts (Constraint) 

-- |Existential wrapper 
data Some :: (* -> Constraint) -> * where 
    Some :: f a => { unSome :: a } -> Some f 

我知道Constraint代表了一種從*不同，可以用來進行分類，似乎一個=>左側上下文類型。

但是在什麼意義上是Some存在封裝？它怎麼可以這樣使用？

Answer 1

並不像它的奇怪GADT /記錄語法應該編譯不談，我們可以瞭解什麼是通過設置f ~ Eq怎麼回事：

Some :: Eq a => a -> Some Eq 

所以，給定一個Eq uatable的事情，我們得到Some Eq它是可用的東西。讓我們將這個應用到'a' :: Char，看看會發生什麼：

(Some :: Eq Char => Char -> Some Eq) ('a' :: Char) :: Some Eq 

正如你所看到的，我們已經「遺忘」的確切類型的價值，但「記住」這是Eq uatable。

的您提供GADT是一個簡單的從Eq的這個推廣到任何與實物* -> Constraint：

(Eq :: * -> Constraint) (Char :: *) :: Constraint 
(f :: * -> Constraint) (a :: *) :: Constraint 

至於爲什麼它被稱爲「生存」，在GADT揣在構造函數聲明的隱含forall：

Some :: forall a. f a => { unSome :: a } -> Some f 

一旦Some f你的模式匹配，你f a => a類型，其中a無法逃脫它的範圍因技術原因的值。 （這被稱爲skolem）您可以使用CPS組合子像這樣與它的工作：

ambiguously :: (forall s. f s => s -> r) -> Some f -> r 
ambiguously f (Some s) = f s 

現在你有ambiguously show :: Some Show -> String，這表明Some Show能的事情。因爲它是不明確的，其中實際類型它使用它被稱爲「模棱兩可」（即它爲ambiguously show $ Some 'a'和ambiguously show $ Some "asdf"）

我們不能做

disambiguate :: f a => Some f -> a 
disambiguate (Some a) = a 

因爲上述斯科倫限制。

My (unpublished) library與此相關，甚至更一般的類型。