haskell - 模式匹配推断类型

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 。这实际上是两件事共同作用的结果:可怕的 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 ，但这是更简单的通用量化类型，而不是您想要的存在量化类型。