Haskell type inference results in error message pointing at the wrong variable-CodePudding

loading the following code in ghci

{-# OPTIONS_GHC -Wall   #-}


--following gives a type error about the arg int not str
bug ::  String -> Int -> Int 
bug str int =  num 
  where num =  str * 10     int 

-- the following gives a type error about the arg str as expected 
works ::  String -> Int -> Int 
works str int = str * 10     int

that gives the following errors:

:reload
[1 of 1] Compiling Main             ( bugTI.hs, interpreted )

bugTI.hs:6:16: error:
    • Couldn't match type ‘[Char]’ with ‘Int’
      Expected: Int
        Actual: String
    • In the expression: num
      In an equation for ‘bug’:
          bug str int
            = num
            where
                num = str * 10   int
  |
6 | bug str int =  num 
  |                ^^^

bugTI.hs:7:29: error:
    • Couldn't match type ‘Int’ with ‘[Char]’
      Expected: String
        Actual: Int
    • In the second argument of ‘( )’, namely ‘int’
      In the expression: str * 10   int
      In an equation for ‘num’: num = str * 10   int
  |
7 |   where num =  str * 10     int 
  |                             ^^^

bugTI.hs:10:17: error:
    • Couldn't match type ‘[Char]’ with ‘Int’
      Expected: Int
        Actual: String
    • In the first argument of ‘(*)’, namely ‘str’
      In the first argument of ‘( )’, namely ‘str * 10’
      In the expression: str * 10   int
   |
10 | works str int = str * 10     int
   |                 ^^^
Failed, no modules loaded.

The error for line 7 in the function bug says that it expects int to be a String which makes no sense as it is in an arithmetic expression.

The corresponding err for line 10 in the function works correctly says that it expects str to be an Int which makes sense.

It seems to me that the error for line 7 is at best misleading, at worst (and unlikely) a bug. Can somebody explain why the error points to the wrong variable? I assume there is something I don't understand.

CodePudding user response：

It seems to me that the error for line 7 is at best misleading, at worst (and unlikely) a bug. Can somebody explain why the error points to the wrong variable? I assume there is something I don't understand.

There is nothing "special" about the (*) :: Num a => a -> a -> a, ( ) :: Num a => a -> a -> a, etc. functions. These are just functions defined in the Num typeclass.

You can make other types a member of the Num typeclass as well, this often happens if people define their own numerical-like types.

So you could, if you wanted to, define an instance for Num for a String type, or for a list in general. You could for example encode a number by the length of the list, and thus derive arithmetic on it. Then that would look like:

import Data.List(genericReplicate)

instance Num [a] where
    ( ) = (  )
    
    (*) = (<*)
    
    abs = id
    
    signum = take 1
    
    fromInteger = (`genericReplicate` undefined)
    
    xs - ys = drop (length ys) xs

I agree that this does not make much sense as an instance for Num, but it is is one of the possible ways to implement this.

What Haskell is complaining about is that the two operands and the return type all need to have the same type. Indeed, in the signature Num a => a -> a -> a, the a is used for the two operands and the return type.

Since int has as type Int by the type signature, it means that the two operands of the addition needs to be Ints, and hence the result of str * 10 should be an Int, that is not a problem for 10, but a problem for str. Even if Num [a] would hold, it still means that this would error, since you can not multiply an Int with a Double for example, or add an Integer and Int together.

CodePudding user response：

Haskell does type inference in two "directions" at once.

Bottom-up: by looking at all the parts of an expression, what should be the type of the whole expression
Top-down: by looking at where this expression is used, what type should it have in order to fit into that context

If there is any place where the two do not agree, there will be a type error reported.

GHC's error messages call type it's worked out by "bottom-up" analysis the "actual type", and the type it's worked out by "top-down" analysis the "expected type". But don't be confused by this terminology; it's not that the "actual type" is in any way more "real" or "current" than the "expected type", nor is the "expected type" any more correct than the actual type. It is not telling you that the type should be the expected type but actually is the actual type. It's just telling you that two different lines of analysis lead to a contradiction about what the type of the expression is.

As such, it's kind of absurd to say that one of these error messages is "right" and the other is "wrong". They are both just telling you "these 2 things don't match, and they should". The compiler has no way of knowing which of the two types the expression "should" have if it was really correct; frequently neither of the two will work, no matter what else you change.

In particular, let's look at the type inference going on in the message you don't like:

bugTI.hs:7:29: error:
    • Couldn't match type ‘Int’ with ‘[Char]’
      Expected: String
        Actual: Int
    • In the second argument of ‘( )’, namely ‘int’
      In the expression: str * 10   int
      In an equation for ‘num’: num = str * 10   int
  |
7 |   where num =  str * 10     int 
  |                             ^^^

And for reference the code is:

bug ::  String -> Int -> Int 
bug str int =  num 
  where num =  str * 10     int

So to report a type error at the position indicated, we need to have both an "actual" (bottom-up) and "expected" (top-down) type for this occurence of int. The bottom-up type is easy; we know it's Int because the expression int only consists of a single variable reference, and that variable was declared to have type Int.

The expected type for int here depends on the context. int is occurring as the right operand to , with the left operand being str * 10. has type Num a => a -> a -> a. So to know what type we "expect" for int we need to know what type str * 10 is inferred as.

* has type Num a => a -> a -> a, so str and 10 must have the same type, and the overall expression str * 10 also has that type. 10 can be any type with a Num instance, but str already has a fixed type from the type signature; it is String (AKA [Char]).

Putting that all together, we now know that

the expressions str, 10, int, str * 10, and str * 10 int all must have the same type
str has type String
int has type Int

These 3 facts cannot all be true. So we need to emit an error message

This is the point where you go wrong. You have knowledge of your conceptual ideas about Num - that we do arithmetic on numbers and String isn't a number - so you say clearly we should "expect" Int for all of those, and the error that should be reported is that str has actual type String and expected type Int. But the compiler cannot possible know about your conceptual ideas of that Num is "for". without that, your way of interpreting the code is not any more valid than doing the opposite, saying that all of those expressions are expected to have type str and it's int that doesn't match! Exactly because there is no consistent typing here, there are multiple ways to get "as close as possible" and then report an error. It is essentially arbitrary which form the error takes in the error message; neither is better than the other. So neither one can be the "wrong" error message.¹

Without knowing the really fine details of the type checker implementation, I would hazard a guess based on this that it simply encountered the str * 10 first and "committed" to String at that point; it knows enough even without looking ahead to know that choosing String as the type of both 10 and also of str * 10 is the only possible chance it has of accepting this code, so there is "nothing to lose" by doing that. And then when it later also finds a requirement forcing that same type to also be Int, it reports an error.²

Now you noted in comments that there is also another error under this interpretation that str, 10, and int are all expected to be String. That is the error that this choice will require an instance Num String, and there is no such instance visible to the compiler. It doesn't report that error because it is "behind" this one; the compiler needs to go looking for an Num instance that matches whatever type is chosen for str, 10, and int, but it doesn't make sense to go looking for that instance until after we've decide what instance we're looking for! That requires pinning down the type involved, and having realised that there is no consistent type it's pointless even trying to resolve the Num constraint. This is an error whether or not Num Int or Num String or Num <anything-else> hold true.

¹ As evidence for my claim that which way around the error is reported is arbitrary, I don't even get the same error messages as you when I tried this. I don't know whether it's just a different version of GHC, or whether it would change sometimes even for the same version. But I get an error about int not being String for both bug and works:

foo.hs:6:16: error:
    • Couldn't match type ‘[Char]’ with ‘Int’
      Expected: Int
        Actual: String
    • In the expression: num
      In an equation for ‘bug’:
          bug str int
            = num
            where
                num = str * 10   int
  |
6 | bug str int =  num
  |                ^^^

foo.hs:7:29: error:
    • Couldn't match type ‘Int’ with ‘[Char]’
      Expected: String
        Actual: Int
    • In the second argument of ‘( )’, namely ‘int’
      In the expression: str * 10   int
      In an equation for ‘num’: num = str * 10   int
  |
7 |   where num =  str * 10     int
  |                             ^^^

foo.hs:11:17: error:
    • Couldn't match type ‘[Char]’ with ‘Int’
      Expected: Int
        Actual: String
    • In the expression: str * 10   int
      In an equation for ‘works’: works str int = str * 10   int
   |
11 | works str int = str * 10     int
   |                 ^^^^^^^^^^^^^^^^

foo.hs:11:30: error:
    • Couldn't match type ‘Int’ with ‘[Char]’
      Expected: String
        Actual: Int
    • In the second argument of ‘( )’, namely ‘int’
      In the expression: str * 10   int
      In an equation for ‘works’: works str int = str * 10   int
   |
11 | works str int = str * 10     int
   |

² And I suppose that this doesn't happen in the works case because you don't have the intermediate num definition that can be inferred its own type; instead the str * 10 int expression occurrs in a context where it is known that it should result in Int, because it is directly the return value of the works function that is declared to return Int. Although as I noted in my previous footnote, this doesn't happen when I run it. But that's fine. There is no one correct order in which GHC is required to consider the pieces of information available to it before it notices the inconsistency.