我何时需要使用类型注释？

Question

请考虑以下函数

{-# LANGUAGE TypeFamilies #-}

tryMe :: Maybe Int -> Int -> Int
tryMe (Just a) b = a
tryMe Nothing b  = b

class Test a where
    type TT a
    doIt :: TT a -> a -> a

instance Test Int where
    type TT Int = Maybe Int
    doIt (Just a) b  = a
    doIt (Nothing) b = b

这是有效的

main = putStrLn $ show $ tryMe (Just 2) 25

这并不是

main = putStrLn $ show $ doIt (Just 2) 25
{- 
  • Couldn't match expected type ‘TT a0’ with actual type ‘Maybe a1’
  The type variables ‘a0’, ‘a1’ are ambiguous
-}

但是，如果我为第二个参数指定类型，它就可以工作。

main = putStrLn $ show $ doIt (Just 2) 25::Int

这两个函数的类型签名看起来是一样的。为什么我需要为类型类函数的第二个参数注释类型？此外，如果我仅注释第一个参数为 Maybe Int，它仍然无法工作。为什么？

- Marcelo Lazaroni

---

GHC担心有人可能会定义一个instance Test Integer，这样实例的选择就会变得模糊不清。 - amalloy

GHC和许多编译器一样，允许分离编译：我们可以单独编译每个模块。 GHC不能知道在尚未编译的某个模块中是否有另一个类的实例。因此，如果它承诺只能看到的唯一实例，则是错误的。为告诉它这个承诺是正确的，我们必须约束调用，使其只能与该实例相关联。由于第二个参数中的数字文字可以是任何类型，因此我们必须明确说明它的类型。 - chi

你非常微妙地提出了两个完全不同的问题（“为什么我需要在这个程序中进行类型注释”和“为什么当将类型注释放置在Maybe Int参数上时，类型注释没有产生相同的影响”）。回答者似乎选择忽略第二个问题（也许是正确的），所以你应该为第二个问题发布一个单独的问题。简短的答案是，类型族不是可逆的。 - user2407038

@user2407038，第二个问题可以通过使用一个可逆的类型族或者（可能更好的选择）使用另一个“取反”的类型族来解决。 - dfeuer

Answer 1

当我在Haskell中需要强制类型转换时？

只有在非常模糊的，伪依赖类型的设置中，编译器无法证明两种类型相等但你知道它们是相等的情况下，您可以使用unsafeCoerce将它们强制转换。 （这就像C ++的reinterpret_cast，即它完全绕过了类型系统，并将内存位置视为包含您告诉它的类型。这确实非常不安全！）

然而，这与你所讨论的完全不同。添加本地签名，如::Int并不执行任何转换，它仅仅向类型检查器添加了一个提示。需要这样的提示并不奇怪：你没有指定a应该是什么；show在其输入上是多态的，而doIt在其输出上是多态的。但编译器必须知道它是什么，才能解析相关的TT；选择错误的a可能会导致与预期完全不同的行为。

更令人惊讶的是，有时您确实可以省略这样的签名。这种可能性的原因在于Haskell，尤其是GHCi，具有默认规则。当您编写例如show 3时，您再次具有一个模棱两可的a类型变量，但是GHC会认识到Num约束可以被“自然地”满足Integer类型，因此它只采用那个选择。
默认规则在快速评估REPL中的内容时很方便，但是依赖它们很麻烦，因此我建议您在正式程序中永远不要这样做。 现在，这并不意味着您应该始终向任何子表达式添加:: Int签名。这确实意味着，作为一项规则，您应该致力于使函数参数始终比结果不太多态化。我的意思是：如果可能的话，任何局部类型变量都应该能够从环境中推断出来。然后，只需指定最终结果的类型即可。

很不幸，show 违反了这个条件，因为它的参数与一个根本没有出现在结果中的变量 a 是多态的。所以这是其中一种你无法避免必须有一些签名的函数。

- leftaroundabout

Answer 2

所有这些讨论都很好，但还没有明确说明在Haskell中数值字面量是多态的。你可能知道这一点，但可能没有意识到它与这个问题有关。在表达式中：

doIt (Just 2) 25

25不是Int类型，它的类型是Num a => a，也就是说，它的类型只是某种数字类型，等待额外的信息来确定它的确切类型。而使这个问题棘手的是，具体的选择可能会影响第一个参数的类型。因此，amalloy的评论如下：

GHC担心有人会定义一个instance Test Integer，这样实例的选择就会变得模糊。

当你提供这些信息时——这些信息可以来自参数或结果类型（由于doIt签名中的a -> a部分）——通过编写以下任一内容之一：

doIt (Just 2) (25 :: Int)
doIt (Just 2) 25 :: Int   -- N.B. this annotates the type of the whole expression

那么，特定实例就会被识别。

请注意，您不需要使用类型族来产生这种行为。这是类型类解析的常规做法。以下代码将出现相同的错误，原因也相同。

class Foo a where
    foo :: a -> a

main = print $ foo 42

您可能会想知道为什么这种情况不会发生在类似于以下内容的东西中：

main = print 42

这是一个好问题，lefrtoundabout已经回答了。这与Haskell的默认规则有关，这些规则非常专业，我认为它们只是一个小技巧。

- luqui

---

很好，将 default() 写入 GHCi 会使其无法推断像 42 这样简单的东西，它只会抛出一个类型不明确的错误。 - helq

Answer 3

使用这个表达式：

putStrLn $ show $ tryMe (Just 2) 25

我们有以下起始信息可供使用：

putStrLn :: String -> IO ()
show :: Show a => a -> String
tryMe :: Maybe Int -> Int -> Int
Just :: b -> Maybe b
2 :: Num c => c
25 :: Num d => d

（我在这里使用了不同的类型变量，因此我们可以更轻松地在相同的范围内考虑它们）

类型检查器的工作基本上是找到所有这些变量的选择类型，然后确保参数和结果类型匹配，以及所有必需的类型类实例都存在。

在这里，我们可以看到tryMe应用于两个参数将成为一个Int，因此a（作为show的输入）必须是Int。这需要存在一个Show Int实例；确实存在，所以我们完成了对a的处理。

同样，tryMe想要一个Maybe Int，我们有应用Just的结果。因此，b必须是Int，而我们对Just的使用是Int -> Maybe Int。

Just被应用于2 :: Num c => c。我们决定它必须应用于一个Int，因此c必须是Int。如果我们有Num Int，那么我们就可以做到这一点，而我们确实有，因此c已经处理完毕。

这样就只剩下25 :: Num d => d了。它被用作tryMe的第二个参数，该函数期望一个Int，因此d必须是Int（再次满足Num约束）。

然后我们只需要确保所有参数和结果类型都匹配，这是非常明显的。这主要是重申上面的内容，因为我们通过选择类型变量的唯一可能值来使它们匹配，所以我不会详细介绍它。

现在，这有什么不同吗？

putStrLn $ show $ doIt (Just 2) 25

好的，让我们再次看看所有的组成部分：

putStrLn :: String -> IO ()
show :: Show a => a -> String
doIt :: Test t => TT t -> t -> t
Just :: b -> Maybe b
2 :: Num c => c
25 :: Num d => d

show函数的输入是应用两个参数到doIt的结果，因此它是t。所以我们知道a和t是相同类型的，这意味着我们需要Show t，但我们还不知道t是什么，所以我们需要回过头来看一下。

应用Just的结果用于需要TT t的地方。所以我们知道Maybe b必须是TT t，因此Just :: _b -> TT t。我使用了GHC的部分类型签名语法来写_b，因为这个_b与之前的b不同。当我们有Just :: b -> Maybe b时，我们可以选择任何我们喜欢的类型来代替b，而Just可以具有该类型。但现在我们需要一些特定但未知的类型_b，使得TT t是Maybe _b。我们没有足够的信息来知道那个类型是什么，因为我们不知道我们正在使用哪个实例的TT t定义，因为我们不知道t是什么。 Just的参数是2 :: Num c => c。所以我们可以知道c也必须是_b，这也意味着我们将需要一个Num _b实例。但由于我们还不知道_b是什么，所以我们无法检查是否有Num实例可用。我们稍后会回来看它。

最后，25 :: Num d => d在doIt想要一个t的地方使用。好的，所以d也是t，我们需要一个Num t实例。同样地，我们仍然不知道t是什么，所以我们无法检查这一点。

所以总体而言，我们已经找出了这些：

putStrLn :: String -> IO ()
show :: t -> String
doIt :: TT t -> t -> t
Just :: _b -> TT t
2 :: _b
25 :: t

同时还有以下待解决的限制条件：

Test t, Num t, Num _b, Show t, (Maybe _b) ~ (TT t)

如果您之前没有看到过，~是我们编写的两个类型表达式必须相同的约束条件。

然后我们就卡住了。我们无法进一步确定，因此GHC将报告类型错误。您引用的特定错误消息抱怨我们无法确定TT t和Maybe _b是否相同（它将类型变量称为a0和a1），因为我们没有足够的信息选择它们的具体类型（它们是模糊的）。

如果我们为表达式的某些部分添加一些额外的类型签名，我们可以更进一步。添加25 :: Int¹可以立即让我们知道t是Int。现在我们可以有所作为！让我们将其修补到我们尚未解决的约束中：

Test Int, Num Int, Num _b, Show Int, (Maybe _b) ~ (TT Int)

Num Int和Show Int是显而易见的内置函数。我们还有Test Int，这给了我们定义TT Int = Maybe Int。因此，(Maybe _b) ~ (Maybe Int)，因此_b也是Int，这也使我们能够解决Num _b限制（它又是Num Int）。现在，由于我们已经将所有类型变量填充为具体类型，因此很容易验证所有参数和结果类型是否匹配。

但是为什么你的其他尝试没有成功？让我们回到没有附加类型注释的最远点：

putStrLn :: String -> IO ()
show :: t -> String
doIt :: TT t -> t -> t
Just :: _b -> TT t
2 :: _b
25 :: t

此外还需要解决以下限制：

Test t, Num t, Num _b, Show t, (Maybe _b) ~ (TT t)

然后添加Just 2 :: Maybe Int。因为我们知道它也是Maybe _b和TT t，这告诉我们_b是Int。我们现在也知道我们正在寻找一个Test实例，它给出了TT t = Maybe Int。但这并不能确定t是什么！有可能还有以下情况：

instance Test Double where
    type TT Double = Maybe Int
    doIt (Just a) _ = fromIntegral a
    doIt Nothing b = b

现在可以将t选择为Int或Double，两者都可以正常工作（因为25也可以是Double），但会打印不同的内容！

诱人的想法是抱怨因为只有一个实例t符合TT t = Maybe Int，所以我们应该选择它。但是实例选择逻辑没有这样猜测。如果你面临的情况可能存在另一个匹配实例，但由于代码错误而不存在（例如忘记导入定义它的模块），那么它不会选择唯一可见的匹配实例。只有当它知道没有其他实例可以适用时，才会选择实例。

因此，“只有一个实例符合TT t = Maybe Int”的论点不能让GHC倒推出t可以是Int。

总的来说，对于类型族，你只能“向前工作”；如果你知道你正在应用类型族的类型，你可以从中得出结果类型应该是什么，但是如果你知道结果类型，这并不能确定输入类型。这通常很令人惊讶，因为普通的类型构造函数确实让我们可以这样“向后工作”；我们使用上面的方法从Maybe _b = Maybe Int推断出_b = Int。这只有在新的data声明中适用，应用类型构造函数始终保留结果类型中的参数类型（例如，当我们将Maybe应用于Int时，结果类型为Maybe Int）。相同的逻辑在类型族中不起作用，因为可能存在多个类型族实例映射到相同的类型，即使没有，也没有要求结果类型中的某些内容与输入类型之间存在可识别的模式（我可以使用type TT Char = Maybe (Int -> Double, Bool)）。

因此，当您需要添加类型注释时，通常会发现在其类型为类型族结果的位置添加注释无法正常工作，而需要确定类型族的输入（或其他必须与其相同类型的内容）。

¹ 请注意，在您的问题中引用的代码 main = putStrLn $ show $ doIt (Just 2) 25::Int 实际上是行不通的。 :: Int 签名绑定“尽可能远”，因此您实际上声称整个表达式 putStrLn $ show $ doIt (Just 2) 25 的类型为 Int，但它必须是 IO () 类型。我假设您在真正检查时在 25 :: Int 周围加上了括号，所以应该是 putStrLn $ show $ doIt (Just 2) (25 :: Int)。

² GHC 有关于什么被认为是“确定的知识”以至于不存在其他匹配实例的特定规则。我不会详细讲解，但基本上当您有 instance Constraints a => SomeClass (T a) 时，它必须能够通过仅考虑 SomeClass (T a) 来明确选择一个实例; 它不能看左边的约束条件 => 符号。

- Ben