haskell - 什么是 AllowAmbiguousTypes，为什么在这个 "forall"示例中需要它？

Question

编码

{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}

-- I know this particular example is silly.
-- But that's not the point here.
g :: forall a . RealFloat a => Bool
g = True

main :: IO ()
main = print (g @Double)

无法在 GHC 8.0 上编译并出现错误

• Could not deduce (RealFloat a0)
      from the context: RealFloat a
        bound by the type signature for:
                   g :: RealFloat a => Bool
        at app/Main.hs:3:6-35
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘g’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        g :: forall a. RealFloat a => Bool

所以添加 AllowAmbiguousTypes将使代码编译。

以下是我的问题:

AllowAmbiguousTypes到底是什么?

为什么需要使这个特定的代码工作？

我担心添加 AllowAmbiguousTypes在这个特定的代码中给了我比我真正想要的更多。听起来很吓人。听起来这会使 Haskell 的类型系统变得不那么安全，也许在与此特定代码无关的其他领域。这些恐惧是没有根据的吗？

有没有其他选择？在这种情况下，Haskell 似乎插入了 a0我从未要求过的类型变量。是否没有扩展告诉 Haskell 不要创建这些无关的类型变量 - 并且只使用我明确告诉它添加的那些我自己明确的 forall a ?

由于 user2407038 增加了一个问题的评论:你会说AllowAmbiguousTypes用词不当？将它命名为 AllowUnusedTypeVariables 会更好吗？ ?

Answer 1

What exactly is AllowAmbiguousTypes?

来自 latest GHC docs , “类型 ty 是模棱两可的当且仅当 ((undefined :: ty) :: ty) 无法进行类型检查”。扩展 AllowAmbiguousTypes只是禁用此检查 - 它不会允许错误类型的程序通过。

Why is it needed to make this particular code work?

为了检查 RealFloat a满足g使用，GHC需要知道什么a是。你没有办法(在 vanilla Haskell1 中)告诉 GHC 什么 a应该是因为 a g 类型中没有其他地方出现.再多的注释都不会让你使用g不会出现模棱两可的类型变量错误。

但是，如果您不使用 g在任何地方，您仍然可以通过打开 AllowAmbiguousTypes 来编译您的代码。 .

I fear that adding AllowAmbiguousTypes is giving me more than I really want in this particular code. It sounds scary. It sounds like it will make Haskell's type system less safe, perhaps in other areas that have nothing to do with this particular code. Are these fears unfounded?

是的，它们是:歧义检查使您可以捕获无法使用的定义(在 vanilla Haskell 中，它没有 TypeApplications 1)，而不会导致模棱两可的类型变量错误。禁用此检查仅意味着当您使用表达式(或函数)而不是在其定义站点时，您将看到模棱两可的类型变量消息。

Are there any alternatives? In this case, it seems like Haskell is inserting a a0 type variable that I never asked for. Is there no extension to tell Haskell not to create these extraneous type variables - and only use those that I explicitly told it to add with my own explicit forall a?

a0来自我在这个答案开头提到的歧义检查。 GHC 仅使用名称 a0明确表示它与 a 不同.歧义检查基本上只是尝试进行类型检查

((undefined :: forall a. RealFloat a => Bool) :: forall a0. RealFloat a0 => Bool)

AllowAmbiguousTypes删除此检查。我不认为有一个扩展只对具有显式 forall 的类型签名禁用歧义检查。 s (虽然这可能是整洁和有用的!)。

Would you say that AllowAmbiguousTypes is a misnomer? Would it have been better named as AllowUnusedTypeVariables?

命名事物是困难的。 :)

当前名称引用了未启用扩展程序时出现的错误类型，因此它不是一个坏名称。我想这是一个见仁见智的问题。 (很多人也希望 Monad 被称为 FlatMapAble 。)

1 之前 TypeApplications (这是 GHC 8.0 的一个相对较新的扩展)，确实没有办法使用触发歧义检查的表达式而不会出现歧义类型变量错误，所以 AllowAmbiguousTypes没那么有用了。