为什么使用模式匹配构造的函数具有Eq类型约束,但在使用数据构造函数时却没有？

Question

为什么ghci 在我通过模式匹配构造的函数的类型签名中列出了一个相等类型约束matchInt:

$ ghci
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> :{
Prelude| matchInt 1 = 3
Prelude| matchInt _ = 4
Prelude| :}
Prelude> matchInt 1
3
Prelude> matchInt 22
4
Prelude> :t matchInt
matchInt :: (Eq a, Num a, Num p) => a -> p

相反,当使用简单的数据构造函数时,没有相等类型约束.

$ ghci
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> data Z = Y Int
Prelude> :{
Prelude| matchDataInt (Y 1) = 3
Prelude| matchDataInt _ = 4
Prelude| :}
Prelude> matchDataInt (Y 1)
3
Prelude> matchDataInt (Y 22)
4
Prelude> :t matchDataInt
matchDataInt :: Num p => Z -> p

实际上Z的实例无法比较:

Prelude> Y 22 == Y 33
<interactive>:11:1: error:
    • No instance for (Eq Z) arising from a use of ‘==’
    • In the expression: Y 22 == Y 33
      In an equation for ‘it’: it = Y 22 == Y 33

那么,为什么matchInt函数列表相等作为类型约束而不是函数matchDataInt呢？

这个问题是相关的.但是,如果需要进行相等测试matchInt那么为什么不需要matchDataInt呢？在这里,我来我的关键点:不都 matchInt和matchDataInt要测试对1匹配操作模式？

Answer 1

语法matchInt上建立在模式匹配上,但这里的模式匹配是一种幻觉.1不是数据构造函数.数字文字被重载.1相当于fromInteger #1哪里#1是类型的非重载的litteral(在标准的Haskell中不可表达)Integer.你无法真正模仿这种事情.

所以编译器允许你在语法上写出模式匹配,但这种表示法真的表示一个守护:

matchInt 1 = ... -- what is written
matchInt x | x == fromInteger #1 = ...  -- what it really means

由于matchInt未明确给出类型,因此推断出它.它是一个函数,所以类型是一些改进a->b.调用fromInteger会产生约束Num a,而调用==会产生约束Eq a,这就是我们所能说的a.

如果OTOH我们给函数一个明确的签名,比方说

matchInt :: Int->Int

那么我们不需要推断类型,只检查它是否满足约束条件.由于Int同时满足Eq Int和Num Int,一切正常.

这就是你的第二个例子中正在发生的事情.您所匹配的类型是已知的Int,不是因为显式类型签名,而是因为它是从Y Int替代中推断出来的Z.这里再次Int已经拥有了所有需要的实例.

Answer 2

该matchDataInt函数不需要Eq约束,因为它在a上特别匹配Int,并且Ints已经有一个Eq实例.

你的matchInt函数不只是将Ints作为参数 - 它可以采用任何类型的数字,只要你可以比较该数字是否相等.这就是为什么它有类型(Eq a, Num a, Num p) => a -> p.你也可以给它的类型Num p => Int -> p(专门a到Int),因为Int已经Eq和Num实例.

matchDataInt另一方面,你的函数Z作为一个参数,每个都Z包含一个Int.针对模式匹配的是Int招致的Eq约束,但只对Int.你可以改为

data Z' a = Y' a

matchDataNum :: (Eq a, Num a, Num p) => Z' a -> p
matchDataNum (Y' 1) = 3
matchDataNum _      = 4

在这里,您无法删除Eq a约束.

对于不自行返回数字的变体函数,这一切可能会更加清晰.如果我们有

data Z    = Y  Int
data Z' a = Y' a

is1 1 = True
is1 _ = False

isY1 (Y 1) = True
isY1 _     = False

isY'1 (Y' 1) = True
isY'1 _      = False

那么我们定义的三个函数都有类型

is1   :: (Eq a, Num a) => a -> Bool
isY1  :: Z -> Bool
isY'1 :: (Eq a, Num a) => Z' a -> Bool

我们也可以定义

is1Int :: Int -> Bool
is1Int 1 = True
is1Int _ = False