我什么时候需要类型注释？

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的第一个参数，它仍然不能工作。为什么？

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根本没有出现在结果中。因此，这是一个功能，你不会有一些签名。

Answer 2

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

doIt (Just 2) 25

25没有Int类型，它有类型Num a => a --也就是说，它的类型只是一些数字类型，等待额外的信息来精确地确定它。让这个问题变得棘手的是，具体的选择可能会影响第一个参数的类型。因此，阿姆的评论

GHC担心有人可能会定义instance Test Integer，在这种情况下，实例的选择将是不明确的。

当您通过编写任何一个参数或结果类型(因为a -> a部分的doIt签名)提供该信息时，

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

这是一个很好的问题，左撇子已经解决了。这与Haskell的违约规则有关，它是如此的专业化，以至于我认为它们不过是一次黑客攻击。