消失約束的情況：較高等級類型的奇異點

Question

下面描述的所有實驗都是用GHC 8.0.1完成的。

此問題是RankNTypes with type aliases confusion的後續行動。這個問題有歸結爲類型的像這樣的功能...

{-# LANGUAGE RankNTypes #-} 

sleight1 :: a -> (Num a => [a]) -> a 
sleight1 x (y:_) = x + y 

...這是由類型檢查被拒絕......

ThinAir.hs:4:13: error: 
    * No instance for (Num a) arising from a pattern 
     Possible fix: 
     add (Num a) to the context of 
      the type signature for: 
      sleight1 :: a -> (Num a => [a]) -> a 
    * In the pattern: y : _ 
     In an equation for `sleight1': sleight1 x (y : _) = x + y 

...因爲higher-排名限制Num acannot be moved outside of the type of the second argument（如果我們改爲a -> a -> (Num a => [a])，將是可能的）。既如此，我們最終要更高秩約束添加到已經量化了整個事情的變量，那就是：

sleight1 :: forall a. a -> (Num a => [a]) -> a 

有了這個概括做，我們會盡量簡化例子一點。讓我們來代替(+)的東西，不需要Num，並從該結果的脫開問題的參數的類型：

sleight2 :: a -> (Num b => b) -> a 
sleight2 x y = const x y 

這不就像工作之前（保存在錯誤略有變化消息）：

ThinAir.hs:7:24: error: 
    * No instance for (Num b) arising from a use of `y' 
     Possible fix: 
     add (Num b) to the context of 
      the type signature for: 
      sleight2 :: a -> (Num b => b) -> a 
    * In the second argument of `const', namely `y' 
     In the expression: const x y 
     In an equation for `sleight2': sleight2 x y = const x y 
Failed, modules loaded: none. 

使用const這裏，然而，也許是不必要的，所以我們可能會嘗試寫自己的實現：

sleight3 :: a -> (Num b => b) -> a 
sleight3 x y = x 

令人驚訝的是，這實際上有效！

Prelude> :r 
[1 of 1] Compiling Main    (ThinAir.hs, interpreted) 
Ok, modules loaded: Main. 
*Main> :t sleight3 
sleight3 :: a -> (Num b => b) -> a 
*Main> sleight3 1 2 
1 

更奇怪的是，似乎有沒有實際Num上的第二個參數約束：

*Main> sleight3 1 "wat" 
1 

我不太清楚如何作出這樣的理解。也許我們可以這樣說，就像我們可以在的範圍內一樣，只要我們從不評價它，只要它不用於統一右側的任何地方，那麼一個不可滿足的約束就可以堅持在一種類型中。然而，這感覺就像是一個非常弱的類比，特別是因爲我們通常認爲非嚴格性是一種涉及價值而不是類型的概念。此外，這讓我們從掌握世界String與Num b => b如何統一 - 假設這種事實際上發生了，我並不十分確定。那麼，什麼是一個準確的描述當約束似乎以這種方式消失的時候呢？

Answer 1

哦，它會變得怪異：

Prelude> sleight3 1 ("wat"+"man") 
1 
Prelude Data.Void> sleight3 1 (37 :: Void) 
1 

看到，有是對這樣的說法實際Num約束。只是，因爲（正如chi已經評論過的）b處於協變位置，所以在調用sleight3時，這不是您必須提供的限制。相反，你可以選擇任何類型的b，然後不管它是什麼，sleight3將爲它提供一個Num實例！

那麼，顯然這是假的。 sleight3不能爲字符串提供了這樣一個num實例，絕大部分絕對不是Void。但它也不會實際上需要，因爲，就像你說的那樣，該約束將適用的論據從不被評估。回想一下，約束多態值本質上只是字典參數的函數。 sleight3只是承諾提供這樣一個字典，然後它實際上使用y，但它然後它不以任何方式使用y，所以它很好。

它基本上是相同的，與這樣的功能：

defiant :: (Void -> Int) -> String 
defiant f = "Haha" 

再次，參數功能顯然不可能產生一個Int，因爲不存在一個Void值與對其進行評估。但是這也不是必需的，因爲f簡直被忽略了！

相比之下，sleight2 x y = const x y確實有點兒八九不離十使用y：第二個參數const僅僅是一個等級0類型，所以編譯器需要在這一點上，以解決任何需要的字典。即使const最終也拋出y，它仍然「足夠」這個價值，使它顯然不是很好的類型。