模式匹配推斷類型

爲什麼不在下面的類型檢查？ _的類型被推斷爲Double。模式匹配推斷類型

{-# LANGUAGE ScopedTypeVariables, Rank2Types #-} 

module Main (main) where 

data D a = D a 

main = 
    let 
    n = D (1 :: forall a. (Floating a) => a) 
    in 
    case n of 
     D (_ :: forall a. (Floating a) => a) -> return()

來源

2017-01-02 denormal

Haskell不支持'D（forall a。（Floating a）=> a）'這樣的類型，它看起來像你在'n'這裏實際需要的類型，因爲這需要impandicative多態性。雖然'1'在這裏確實是多態的，但由於Haskell的類型默認規則（否則該類型將被認爲是不明確的），「D 1」仍然默認爲「D Double」。 –

看來，你正期待着n類型是D (forall a. (Floating a) => a)，但就是強調不所推斷的類型。事實上，如果您嘗試將該類型註釋添加到n，您會發現GHC會大聲抱怨。這種類型需要GHC支持impandicative多態性，它目前不（有關更多信息，請參閱What is predicativity?）。

實際推斷爲n的類型是D Double。這實際上是兩件事情的結果：可怕的monomorphism restriction和Haskell的類型違約規則。由於單態的限制，n必須被推斷爲單態類型（因爲它不是語法上的函數，也沒有明確的類型註釋）。由於這個原因，D 1將是不明確的，因爲1 :: forall a. (Floating a) => a是多態的。然而，在這種情況下，Haskell已經違反了數字類型的規則，主要是爲了避免解決由於Haskell的多態數字文字造成的歧義。

由於您明確將類型註釋添加到1以使其成爲Floating，因此Haskell將其默認規則應用於浮點類型，並且默認爲Double。因此，n的類型被推斷爲D Double。

如果您禁用單態限制，那麼n的類型將是更有趣的類型forall a. Floating a => D a，但這是更簡單的普遍量化類型，而不是您想要的存在量化類型。

來源

2017-01-02 19:09:50

模式匹配推斷類型

回答

相關問題