Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why does a function constructed with pattern matching have the Eq type constraint but not when using a data constructor?

Why does ghci list an equality type constraint in the type signature for this function matchInt which I constructed via pattern matching:

$ 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

In contrast, when using a simple data constructor, there is no equality type constraint.

$ 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

Indeed instances of Z can not be compared:

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

So again, why does the matchInt function list equality as a type constraint but not the function matchDataInt?

This question is related. However, if an equality test is needed for matchInt then why isn't it needed for matchDataInt? And here I come to my key point: don't both matchInt and matchDataInt have to test against 1 for the pattern matching to operate?

like image 364
Rick Majpruz Avatar asked Oct 25 '17 05:10

Rick Majpruz


2 Answers

Syntactically matchInt is built on a pattern match, but the patern match here is an illusion. 1 is not a data constructor. Numeric literals are overloaded. 1 is equivalent to fromInteger #1 where #1 is a non-overloaded litteral (not expressible in standard Haskell) of type Integer. You cannot really pattern match against such things.

So the compiler lets you write what is syntactically a pattern match, but this notation really denotes a guard:

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

Since the type of matchInt is not explicitly given, it's inferred. It's a function, so the type is some refinement of a->b. The call to fromInteger gives rise to the constraint Num a, and the call to == gives rise to the constraint Eq a, and that's all we can tell about a.

If OTOH we give the function an explicit signature, say

matchInt :: Int->Int

then we don't need to infer the type, but only check if it satisfies the constraints. Since Int satisfies both Eq Int and Num Int, everything is ok.

And this is what's going on in your second example. The type you match is known to be Int, not because of an explicit type signature but because it is inferred from the Y Int alternative of Z. Here again Int already has all the needed instances.

like image 62
n. 1.8e9-where's-my-share m. Avatar answered Nov 10 '22 05:11

n. 1.8e9-where's-my-share m.


The matchDataInt function doesn't require an Eq constraint because it specifically matches on an Int, and Ints already have an Eq instance.

Your matchInt function doesn't just take Ints as parameters – it can take any kind of number, as long as you can compare that number for equality. That's why it has type (Eq a, Num a, Num p) => a -> p. You could also give it the type Num p => Int -> p (specializing a to Int), because Int already has Eq and Num instances.

Your matchDataInt function, on the other hand, takes a Z as an argument, and every Z contains an Int. Pattern matching against that Int incurs an Eq constraint, but only on the Int. You could instead have

data Z' a = Y' a

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

And here, you couldn't remove the Eq a constraint.


This all might be slightly clearer with variant functions that didn't return numbers themselves. If we have

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

then the three functions we've defined have the types

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

We could also define

is1Int :: Int -> Bool
is1Int 1 = True
is1Int _ = False
like image 43
Antal Spector-Zabusky Avatar answered Nov 10 '22 05:11

Antal Spector-Zabusky