Haskell 整数文字如何在不在 Eq 类中的情况下进行比较?

2024-02-25

在 Haskell 中(至少在 GHC v8.8.4 中),Num类确实NOT暗示着处于Eq class:

$ ghci
 GHCi, version 8.8.4: https://www.haskell.org/ghc/  :? for help
 λ> 
 λ> let { myEqualP :: Num a => a -> a -> Bool ; myEqualP x y = x==y ; }

<interactive>:6:60: error:
    • Could not deduce (Eq a) arising from a use of ‘==’
      from the context: Num a
        bound by the type signature for:
                   myEqualP :: forall a. Num a => a -> a -> Bool
        at <interactive>:6:7-41
      Possible fix:
        add (Eq a) to the context of
          the type signature for:
            myEqualP :: forall a. Num a => a -> a -> Bool
    • In the expression: x == y
      In an equation for ‘myEqualP’: myEqualP x y = x == y
 λ> 

看来这是因为例如Num实例可以定义为一些功能类型 https://stackoverflow.com/questions/18676468/could-not-deduce-eq-a-from-num-a-or-from-floating-a-but-can-deduce-eq-a.

此外,如果我们阻止ghci由于过度猜测整数文字的类型,它们只有Num类型约束:

 λ> 
 λ> :set -XNoMonomorphismRestriction
 λ> 
 λ> x=42
 λ> :type x
 x :: Num p => p
 λ> 

因此,像上面的 x 或 42 这样的术语没有理由具有可比性。

但他们仍然碰巧是:

 λ> 
 λ> y=43
 λ> x == y
 False
 λ> 

有人可以解释这个明显的悖论吗?


如果不使用则无法比较整数文字Eq。但实际情况也并非如此。

In GHCi, under NoMonomorphismRestriction (which is default in GHCi nowadays; not sure about in GHC 8.8.4) x = 42 results in a variable x of type forall p :: Num p => p.1

Then you do y = 43, which similarly results in the variable y having type forall q. Num q => q.2

Then you enter x == y, and GHCi has to evaluate in order to print True or False. That evaluation cannot be done without picking a concrete type for both p and q (which has to be the same). Each type has its own code for the definition of ==, so there's no way to run the code for == without deciding which type's code to use.3

However each of x and y can be used as any type in Num (because they have a definition that works for all of them)4. So we can just use (x :: Int) == y and the compiler will determine that it should use the Int definition for ==, or x == (y :: Double) to use the Double definition. We can even do this repeatedly with different types! None of these uses change the type of x or y; we're just using them each time at one of the (many) types they support.

Without the concept of defaulting, a bare x == y would just produce an Ambiguous type variable error from the compiler. The language designers thought that would be extremely common and extremely annoying with numeric literals in particular (because the literals are polymorphic, but as soon as you do any operation on them you need a concrete type). So they introduced rules that some ambiguous type variables should be defaulted to a concrete type if that allows compilation to continue.5

那么当你这样做时实际发生了什么x == y是编译器只是选择Integer用于x and y在该特定表达式中,因为您没有为其提供足够的信息来确定任何特定类型(并且因为默认规则适用于这种情况)。Integer has an Eq实例,因此它可以使用它,即使最常见的类型x and y不包括Eq约束。无需采摘某物它甚至不可能尝试调用==(当然,它选择的“东西”必须位于Eq不然还是不行)。

If you turn on -Wtype-defaults (which is included in -Wall), the compiler will print a warning whenever it applies defaulting6, which makes the process more visible.


1 The forall p part is implicit in standard Haskell, because all type variables are automatically introduced with forall at the beginning of the type expression in which they appear. You have to turn on extensions to even write the forall manually; either ExplicitForAll just for the ability to write forall, or any one of the many extensions that actually add functionality that makes forall useful to write explicitly.


2 GHCi will probably pick p again for the type variable, rather than q. I'm just using a different one to emphasise that they're different variables.


3 Technically it's not each type that necessarily has a different ==, but each Eq instance. Some of those instances are polymorphic, so they apply to multiple types, but that only really comes up with types that have some structure (like Maybe a, etc). Basic types like Int, Integer, Double, Char, Bool, each have their own instance, and each of those instances has its own code for ==.


4 In the underlying system, a type like forall p. Num p => p is in fact much like a function; one that takes a Num instance for a concrete type as a parameter. To get a concrete value you have to first "apply the function" to a type's Num instance, and only then do you get an actual value that could be printed, compared with other things, etc. In standard Haskell these instance parameters are always invisibly passed around by the compiler; some extensions allow you to manipulate this process a little more directly.

这就是令人困惑的根源x == y工作时x and y是多态变量。如果您必须显式传递类型/实例参数,那么这里发生的情况就会很明显,因为您必须手动应用这两个参数x and y并比较结果。


5 The gist of the default rules is that if the constraints on an ambiguous type variable are:

  1. 所有内置类
  2. 其中至少有一个是数字类(Num, Floating, etc)

那么GHC会尝试Integer查看该类型是否检查并允许解决所有其他约束。如果这不起作用,它将尝试Double,如果这不起作用then它报告一个错误。

您可以设置它将尝试的类型default声明(“默认默认值”是default (Integer, Double)),但您无法自定义它尝试默认设置的条件,因此根据我的经验,更改默认类型的用处有限。

然而 GHCi 附带扩展默认规则 https://downloads.haskell.org/ghc/latest/docs/html/users_guide/ghci.html#extension-ExtendedDefaultRules这在解释器中更有用(因为它必须逐行进行类型推断,而不是立即对整个模块进行类型推断)。您可以在编译代码中打开它们ExtendedDefaultRules扩展(或在 GHCi 中关闭它们)NoExtendedDefaultRules),但是根据我的经验,这两个选项都不是特别有用。解释器和编译器的行为不同是很烦人的,但是一次模块编译和一次一行解释之间的根本区别意味着切换其中一个的默认规则以与另一个一致地工作更加烦人。 (这也是为什么NoMonomorphismRestriction现在在解释器中默认生效;单态限制在编译代码中实现其目标方面做得不错,但在解释器会话中几乎总是错误的)。


6 You can also use a typed hole in combination with the asTypeOf helper https://hackage.haskell.org/package/base-4.15.0.0/docs/Prelude.html#v:asTypeOf to get GHC to tell you what type it's inferring for a sub-expression like this:

λ :t x
x :: Num p => p

λ :t y
y :: Num p => p

λ (x `asTypeOf` _) == y

<interactive>:19:15: error:
    • Found hole: _ :: Integer
    • In the second argument of ‘asTypeOf’, namely ‘_’
      In the first argument of ‘(==)’, namely ‘(x `asTypeOf` _)’
      In the expression: (x `asTypeOf` _) == y
    • Relevant bindings include
        it :: Bool (bound at <interactive>:19:1)
      Valid hole fits include
        x :: forall p. Num p => p
          with x
          (defined at <interactive>:1:1)
        it :: forall p. Num p => p
          with it
          (defined at <interactive>:10:1)
        y :: forall p. Num p => p
          with y
          (defined at <interactive>:12:1)

你可以看到它告诉我们很好而且简单Found hole: _ :: Integer,然后再继续处理它喜欢向我们提供的有关错误的所有额外信息。

键入的孔(最简单的形式)仅意味着写入_代替表达式。编译器会在这样的表达式上出错,但它会尝试为您提供有关可以使用什么来“填空”以使其编译的信息;最有帮助的是,它告诉您在该位置有效的事物类型。

foo `asTypeOf` bar是添加一些类型信息的旧模式。它返回foo但它限制它(的这种特殊用法)与以下类型相同bar(实际值bar完全未使用)。所以如果你已经有一个变量d与类型Double, x `asTypeOf` d将是x as a Double.

这里我用的是asTypeOf“向后”;我没有使用右边的东西来约束左边的东西的类型,而是在右边放一个洞(可以有任何类型),但是asTypeOf方便地确保它与以下类型相同x在不改变方式的情况下x在整体表达式中使用(因此相同的类型推断仍然适用,包括默认,如果您将较大表达式的一小部分取出来向 GHCi 询问其类型,则情况并不总是如此:t;尤其:t x不会告诉我们Integer, but Num p => p).

本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)

Haskell 整数文字如何在不在 Eq 类中的情况下进行比较? 的相关文章

随机推荐