將有效的所有類型賦給let-bound變量時鍵入錯誤

這是類型檢查器中的錯誤嗎？將有效的所有類型賦給let-bound變量時鍵入錯誤

Prelude> let (x :: forall a. a -> a) = id in x 3 

<interactive>:0:31: 
    Couldn't match expected type `forall a. a -> a' 
       with actual type `a0 -> a0' 
    In the expression: id 
    In a pattern binding: (x :: forall a. a -> a) = id

，上面沒有類型檢查，但這種扭曲成功的事實：

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id 
3

使我認爲「弱prenex轉換」（見this paper 23頁）可能會莫名其妙相關。將forall嵌入一個不能「浮出」的逆變位置似乎可以保證它不會出現這種奇怪的錯誤。

來源

2011-11-18 Tom Crockett

有趣。我在GHC 6.12.1上得到了一個不同的錯誤信息：「推斷的類型比預期的更少多態性。量化類型變量'a'在表達式id：中轉義。 – hammar

我使用GHC 7.2.1，FWIW。 –

我可能是錯的（我在一個更老的GHC），但這不是合法的Haskell 98/2010。你有什麼擴展？這可能解釋發生了什麼。（我得到了與Hammar相同的錯誤，所以問題可能是'a'並不意味着你的期望。） –

我認爲這裏發生的事情是這樣的：在標準的Damas –米爾納類型推斷中，讓綁定是類型泛化發生的唯一地方。您失敗的示例使用的類型簽名是pattern type signature，它「以明顯的方式約束模式的類型」。現在，在這個例子中，這種約束是否應該在泛化之前或之後發生並不「明顯」，但是，我認爲，你的失敗的例子表明它在泛化之前被應用。

將更加具體：在let綁定let x = id in ...，什麼情況是，id的類型forall a. a->a被實例化到一個單一型，說a0 -> a0，然後將其指定爲x的類型，然後概括爲forall a0. a0 -> a0。如果我認爲在泛化之前檢查了模式類型簽名，它實質上是要求編譯器驗證a0 -> a0是否比多態類型forall a. a -> a更普遍，事實並非如此。

如果我們將類型簽名移動到綁定級別，let x :: forall a. a-> a; x = id in ...簽名在泛化之後被檢查（因爲這被允許以允許多態遞歸），並且沒有類型錯誤發生。

無論是不是一個錯誤，我認爲，這是一個意見。似乎沒有一個實際的規範會告訴我們這裏的正確行爲是什麼;只有我們的期望。我建議與GHC人討論此事。

來源

2011-11-19 21:10:19 ibid

謝謝，這聽起來像是一個非常合理的理論。 –

我在GHC trac上提交[此問題]（http://hackage.haskell.org/trac/ghc/ticket/5650）。 –

不是一個真正的答案，但太長的評論：
這可能是一個錯誤。不出所料地玩了一下，不出所料

let x :: forall a. a -> a; x = id in x 3

如果寫入顯式文件被啓用，則可以使用。儘管如此，這是一款符合標準的沼氣標準。其他一些變化：

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 
3

好吧，這工作，我不知道爲什麼拉姆達行爲不同，但它確實。但是：

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables 
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3 

<interactive>:0:31: 
    Couldn't match expected type `t0 -> t1' 
       with actual type `forall a. a -> a' 
    The lambda expression `\ y -> id y' has one argument, 
    but its type `forall a. a -> a' has none 
    In the expression: \ y -> id y 
    In a pattern binding: (x :: forall a. a -> a) = \ y -> id y

（7.2.2; 7.0.4給出了相同的錯誤）。這是令人驚訝的。

來源

2011-11-19 12:13:17

將有效的所有類型賦給let-bound變量時鍵入錯誤

回答

相關問題