存在型包裝的必要性

Question

原來，儘管存在非常簡單的想法，但使用existential/rank-n類型的確很難。

爲什麼要將存在類型打包成data類型是必要的？

我有以下簡單的例子：

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-} 
module Main where 

c :: Double 
c = 3 

-- Moving `forall` clause from here to the front of the type tuple does not help, 
-- error is the same 
lists :: [(Int, forall a. Show a => Int -> a)] 
lists = [ (1, \x -> x) 
     , (2, \x -> show x) 
     , (3, \x -> c^x) 
     ] 

data HRF = forall a. Show a => HRF (Int -> a) 

lists' :: [(Int, HRF)] 
lists' = [ (1, HRF $ \x -> x) 
     , (2, HRF $ \x -> show x) 
     , (3, HRF $ \x -> c^x) 
     ] 

如果我註釋掉的lists定義，代碼編譯成功。如果我不評論它，我會收到以下錯誤：

test.hs:8:21: 
    Could not deduce (a ~ Int) 
    from the context (Show a) 
     bound by a type expected by the context: Show a => Int -> a 
     at test.hs:8:11-22 
     `a' is a rigid type variable bound by 
      a type expected by the context: Show a => Int -> a at test.hs:8:11 
    In the expression: x 
    In the expression: \ x -> x 
    In the expression: (1, \ x -> x) 

test.hs:9:21: 
    Could not deduce (a ~ [Char]) 
    from the context (Show a) 
     bound by a type expected by the context: Show a => Int -> a 
     at test.hs:9:11-27 
     `a' is a rigid type variable bound by 
      a type expected by the context: Show a => Int -> a at test.hs:9:11 
    In the return type of a call of `show' 
    In the expression: show x 
    In the expression: \ x -> show x 

test.hs:10:21: 
    Could not deduce (a ~ Double) 
    from the context (Show a) 
     bound by a type expected by the context: Show a => Int -> a 
     at test.hs:10:11-24 
     `a' is a rigid type variable bound by 
      a type expected by the context: Show a => Int -> a at test.hs:10:11 
    In the first argument of `(^)', namely `c' 
    In the expression: c^x 
    In the expression: \ x -> c^x 
Failed, modules loaded: none. 

爲什麼會發生這種情況？第二個例子不應該等同於第一個例子嗎？這些n-rank類型的用法有什麼區別？當我想要這樣的多態時，是否有可能遺漏額外的ADT定義並僅使用簡單類型？

Answer 1

有兩個問題，你必須考慮關於處理存在的類型：如果您存儲「任何可以show N」，您可以選擇存儲可以與一起顯示的東西

• 如何顯示它。
• 實際變量只能有一個單一類型。

第一點就是爲什麼你必須有生存型包裝器，因爲當你這樣寫：

data Showable = Show a => Showable a 

而實際上，這樣的事情被宣告：

data Showable a = Showable (instance of Show a) a 

即對Show a的類實例的引用將與值a一起存儲。如果沒有這種情況發生，你不能有一個解開Showable的函數，因爲那個函數不知道如何顯示a。例如，第二點就是爲什麼有時候會出現某種類型的古怪，以及爲什麼你不能在綁定中綁定存在類型（existential types）。

---

您的代碼中存在推理問題。如果你有一個函數，如forall a . Show a => (Int -> a)，你可以得到一個函數，給定任何整數，將能夠產生調用者選擇的任何類型的可顯示值。你可能意思是exists a . Show a => (Int -> a)，這意味着如果函數獲得一個整數，它將返回一個存在Show實例的類型。

Answer 2

這些示例並不等同。第一，

lists :: [(Int, forall a. Show a => Int -> a)] 

說，每個第二組分可以產生任何所需類型，只要它是Show實例從Int。

第二個例子是模相當於

lists :: [(Int, exists a. Show a => Int -> a)] 

即類型的包裝中，每個第二組分可以產生一些類型從Int屬於Show，但不知道其中類型起作用的回報。

此外，你投入的元組的功能不滿足第一份合同：

lists = [ (1, \x -> x) 
     , (2, \x -> show x) 
     , (3, \x -> c^x) 
     ] 

\x -> x產生，它是作爲輸入，所以在這裏同類型的結果，這是Int。 show總是生成String，所以它是一個固定類型。最後，\x -> c^x產生與c相同的型號，即Double。

Answer 3

你第一次嘗試使用存在的類型是不。而是你

lists :: [(Int, forall a. Show a => Int -> a)] 

需求，第二組件可以提供的元素的任何 showable類型我選擇，不只是你選擇一些 showable類型。您正在尋找

lists :: [(Int, exists a. Show a * (Int -> a))] -- not real Haskell 

但這不是你說的。數據類型打包方法允許您通過currying從forall中恢復exists。你有

HRF :: forall a. Show a => (Int -> a) -> HRF 

這意味着建立一個HRF值，你必須提供一個含有三型a，一個Show字典a和Int -> a功能。也就是說，HRF構造函數的類型有效咖喱這種非類型

HRF :: (exists a. Show a * (Int -> a)) -> HRF -- not real Haskell 

您可能能夠避免通過使用秩n種堂編碼的存在

type HRF = forall x. (forall a. Show a => (Int -> a) -> x) -> x 

的數據類型的方法，但是這可能矯枉過正。