什么是AllowAmbiguousTypes，为什么需要在这个“forall”例？ [英] What is AllowAmbiguousTypes and why is it needed in this "forall" example?

问题描述

代码

  { - ＃LANGUAGE ScopedTypeVariables，TypeApplications＃ - } 
 
  -  I知道这个特别的例子是愚蠢的。 
  - 但这不是重点。 
 g :: forall a。 RealFloat a => Bool 
g = True 
 
 main :: IO（）
 main = print（g @Double）
  

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

 •无法推导出RealFloat a0）
从上下文：RealFloat a 
绑定类型签名为：
g :: RealFloat a => Bool 
在app / Main.hs：3：6-35 
类型变量'a0'不明确
•在'g'的模糊检查中
为了推迟歧义检查以使用网站，启用AllowAmbiguousTypes 
在类型签名中：
g :: forall a。 RealFloat a => Bool 
  

因此，添加 AllowAmbiguousTypes 编译。

这是我的问题：

• 究竟是 AllowAmbiguousTypes ？


• 为什么需要使这个特定的代码有效？


• 我担心添加 AllowAmbiguousTypes 在这个特定的代码中给了我比我真正想要的更多的东西。听起来很可怕。这听起来似乎会让Haskell的类型系统不太安全，也许在与此特定代码无关的其他领域。这些恐惧是否没有根据？


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


• 由于 user2407038 的评论添加了一个问题：您会说 AllowAmbiguousTypes 是一个用词不当吗？它会被命名为 AllowUnusedTypeVariables ？

解决方案 div>

究竟是什么 AllowAmbiguousTypes ？

从 latest GHC docs ，类型 ty 当且仅当（（undefined :: ty）： ：ty）将无法检查。扩展 AllowAmbiguousTypes 只是禁用此检查 - 它不会允许不良类型的程序通过。

为什么需要使这个特定的代码有效？

为了检查 RealFloat当使用 g 时，满足，GHC需要知道 a 是什么。你没有办法告诉GHC a 应该是自$ a 1 c>在 g 类型中无处可见。没有多少注释可以让你使用 g 而不会得到一个模棱两可的类型变量错误。然而，如果你不在任何地方使用 g ，您仍然可以通过打开 AllowAmbiguousTypes



我担心添加 AllowAmbiguousTypes 会给我更多比我真正想要的在这个特定的代码。听起来很可怕。这听起来似乎会让Haskell的类型系统不太安全，也许在与此特定代码无关的其他领域。这些恐惧是没有根据的吗？

是的他们是：歧义检查让你捕捉不能定义（在香草Haskell中，它不使用 TypeApplications 1 ），而不会导致模糊的类型变量错误。禁用此检查仅意味着当您使用表达式（或函数）而不是定义站点时，您将看到含糊不清的类型变量消息。

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

a0 来自我在本答案开头提到的模糊检查。 GHC只是使用名称 a0 来说明它与 a 不同。歧义检查基本上只是试图检查



 （（undefined :: forall a。RealFloat a => Bool）:: forall a0。RealFloat a0 => Bool）
  

AllowAmbiguousTypes 删除此检查。我不认为有一个扩展可以通过显式 forall s来禁用歧义性检查（尽管这可能是简洁而有用的！）。

你会说 AllowAmbiguousTypes 是一个用词不当吗？它会被命名为 AllowUnusedTypeVariables ？

命名事情很难。 ：）



当前名称引用您在未启用扩展名的情况下获得的错误类型，因此它不是错误的名称。我想这是一个意见问题。 （许多人也希望 Monad 被称为类似于 FlatMapAble 的形式。）

$在 TypeApplications 之前（这是来自GHC的一个相对较新的扩展）。b $ b

---

¹ 8.0），真的没有办法使用触发歧义检查的表达式而没有得到一个模棱两可的类型变量错误，所以 AllowAmbiguousTypes 的用处不大。

The code

{-# 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)

fails to compile on GHC 8.0 with the error

• 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

So adding AllowAmbiguousTypes will make the code compile.

Here are my questions:

• What exactly is AllowAmbiguousTypes?
• Why is it needed to make this particular code work?
• 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?
• 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?
• Added one question because of user2407038's comment: Would you say that AllowAmbiguousTypes is a misnomer? Would it have been better named as AllowUnusedTypeVariables?

解决方案

What exactly is AllowAmbiguousTypes?

From the latest GHC docs, "a type ty is ambiguous if and only if ((undefined :: ty) :: ty) would fail to typecheck". The extension AllowAmbiguousTypes just disables this check - it won't allow ill-typed programs through.

Why is it needed to make this particular code work?

In order to check that RealFloat a is satisfied whenever g is used, GHC needs to know what a is. You have not way (in vanilla Haskell¹) of telling GHC what a should be since a occurs nowhere else in the type of g. No amount of annotations will let you use g without getting an ambiguous type variable error.

However, if you don't use g anywhere, you can still get your code to compile by turning on 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?

Yes they are: the ambiguity check lets you catch definitions which cannot (in vanilla Haskell, which doesn't have TypeApplications¹) be used without resulting in an ambiguous type variable error. Disabling this check just means you will see the ambiguous type variable messages when you use the expression (or function) instead of at its definition site.

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?

The a0 is coming from the ambiguity check I mentioned at the beginning of this answer. GHC just uses the name a0 to make it clear it is different from a. The ambiguity check basically just tries to typecheck

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

AllowAmbiguousTypes removes this check. I don't think there is an extension that disables ambiguity checks only on type signatures with explicit foralls (although this might be neat and useful!).

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

Naming things is hard. :)

The current name references the type of errors you get without the extension enabled, so it isn't a bad name. I guess this is a matter of opinion. (A lot of people also wish Monad was called something like FlatMapAble.)

---

¹ Prior to TypeApplications (which is a relatively new extension from GHC 8.0), there really was no way of using expressions that triggered the ambiguity check without getting an ambiguous type variable error, so AllowAmbiguousTypes was a lot less useful.

这篇关于什么是AllowAmbiguousTypes，为什么需要在这个“forall”例？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！