パターンマッチングの推論型

Question

以下の型チェックはなぜですか？ _のタイプは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() 

Answer 1

は、あなたがnのために期待しているタイプがD (forall a. (Floating a) => a)であることが表示されますが、それはきっぱりない推察されるタイプです。実際に、そのタイプの注釈をnに追加しようとすると、GHCが大きな文句を言うことに気付くでしょう。そのようなタイプは、GHCに証拠のある多型をサポートすることを要求し、現時点ではそうではありません（それが何であるか、それがなぜ複雑であるかの詳細については、What is predicativity?を参照してください）。

nに対して実際に推論されるタイプはD Doubleです。これは実際にプレイ中の2つの結果、つまり恐ろしいmonomorphism restrictionとHaskellのタイプのデフォルトルールの結果です。単相性の制約のために、nは、（それが構文的に関数ではなく、明示的な型の注釈を持たないため）単形型であると推論されなければならない。このため、1 :: forall a. (Floating a) => aは多型であるため、D 1はあいまいです。しかし、この場合、Haskellは数値型のデフォルトルールを持っています。ほとんどの場合、Haskellの多態数リテラルのためにあいまいさを解決する必要がありません。

に型名を明示的に追加してFloatingにするため、Haskellは浮動小数点型のデフォルトルールを適用し、デフォルトはDoubleになります。したがって、nのタイプはD Doubleと推測されます。

monomorphismの制限を無効にすると、nのタイプは、少し面白いタイプforall a. Floating a => D aになりますが、これは、必要に応じて存在する定量化されたタイプではなく、より単純に普遍化されたタイプです。