模式匹配推断类型

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 支持谓词多态性，而目前它不需要（有关它是什么以及它为什么复杂的更多信息，请参阅）。

n实际推断出的类型是D Double。这实际上是两件事在起作用的结果：可怕的和 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，但这是更简单的通用量化类型，而不是你所定义的存在量化类型想要。

模式匹配推断类型

Pattern matching inferred type

haskell

pattern-matching

higher-rank-types