How does Haskell's type system generate this error?
Why is it complaining about
b
whena
comes before it in the expression and is equally wrong?
...why not? You've said yourself that they are both wrong. GHC has also figured out they are both wrong. It's telling you they are both wrong. Also, a
doesn't really come "before", because there is no real concept of "before" and "after" in Haskell. If anything, it's "in-out", not "left-right", and then b
(underneath only a ($)
) is "before" the a
(underneath zip
, (.)
, and ($)
). It doesn't matter, anyway.
In the top-most error, the expected type is
[(Double, Double)]
. Cool, makes sense. But how come the actual type is[(Int, Double)]
? How did the double emerge if botha
andb
are[Int]
?
sum . map _etc . zip a
is expected to have type [Int] -> Double
, because of the type signature and because it's the left side of a ($)
. Drilling deeper, zip a
is supposed to be [Int] -> [(Double, Double)]
. It is actually forall b. [b] -> [(Int, b)]
. Using the argument type, we can choose to set b ~ Int
, thereby deducing that zip a
is actually [Int] -> [(Int, Int)]
(which is true) where a [Double] -> [(Double, Double)]
was expected, or we can choose to set b ~ Double
(from the return type) and decide that, actually, zip a :: [Double] -> [(Int, Double)]
(which is also true). Both ways you get an error. In fact, I think GHC is doing this in a third way, similar to the first, but I'll spare you the details.
The core of the issue is this: in a Haskell program, there are multiple ways to figure out the type of an expression if you know the types of the stuff around or in it. In a well-typed program, all these derivations agree with each other, and, in an ill-typed program, they disagree, usually in multiple ways. GHC simply chooses two of them, calls them "expected" and "actual" in a way that hopefully makes sense, and complains that they disagree. Here, you found a third derivation that is also in conflict with the "expected" derivation, but GHC, for whatever reason, chose not to use your derivation for the "actual type". Choosing which derivation to show is not easy, especially in Haskell, where everything is allowed to affect the type of everything else, though it could definitely be better. Some years ago, one of GHC's leaders did some work on much better error messages, but it appears to have link-rotted slightly—the Haskell-analyzer bridge seems to have link-rotted off the Internet.
If you're faced with an error like this, I would recommend, first of all, not writing in the _ . _ . ... $ _
style. It's easier to follow my main advice if you write that as _ $ _ $ ... $ _
. I won't change it here, but you should keep that in mind.
poly :: [Int] -> [Int] -> Double -> Double
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b
You see an error and it's not immediately obvious what to change. Very well, simply give up trying to decipher the hieroglyphs and replace part(s) of the RHS with _
. The more of the RHS you delete, the better your chance of catching the error, going to ~95% if you erase all of it:
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . _ $ _
-- personally, I'd nuke the scary-looking map _lambda, too,
-- but I'm also trying to keep this short
GHC will tell you that the left _
is meant to be _a -> [(Double, Double)]
, and the right one _a
. Add the zip
:
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip _ $ _
and you'll be told you need two [Double]
s, and you'll realize that using a
and b
didn't work because a, b :: [Int]
(and GHC actually says a :: [Int]; b :: [Int]
in the error message, because sometimes it isn't clear). You then figure out how to fix it:
poly a b x = sum . map (\(ai, bi) -> ai * (x ** bi)) . zip (fromIntegral <$> a) $ fromIntegral <$> b
All is well.
- Why is it complaining about
b
when a comes before it in the expression and is equally wrong?
Well, there are two errors. It complains about zip a
, and it complains about b
. And it issues those errors in the order they appear in the source.
- In the top-most error, the expected type is
[(Double, Double)]
. Cool, makes sense. But how come the actual type is[(Int, Double)]
? How did the double emerge if botha
andb
are[Int]
?
Not so fast. The actual type in that error is not [(Int, Double)]
. It says that zip a
is wrong, and its says the expected type is [Double] -> [(Double, Double)]
, while the actual type is [Double] -> [(Int, Double)]
. That's not the same thing as there being an expression which is expected to be of type [(Double, Double)]
and actually is of type [(Int, Double)]
.
zip a
is a function. We know it's supposed to return [(Double, Double)]
(because the rest of the composition chain processes that to return the final Double
result from poly
.
The remaining parameter of the function zip a
needs to be of type [Double]
(by the type of zip
) in order for the return type to fit [(Double, Double)]
, and that's fine; zip a
can take a [Double]
argument.
The problem is that zip a
is not a function of type [Double] -> [(Double, Double)]
; the closest it could manage is [Double] -> [(Int, Double)]
, because of the use of a
in the expression zip a
. So that's what the error complains about.
You're asking why it doesn't complain about [(Int, Int)]
instead of [(Int, Double)]
, since that's what you'd get if you applied zip a
to b
. But nowhere in your code do you do that! You apply the whole function sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a
to b
(via the $
operator). The type error is not complaining about zip a b
being the wrong type of list, it's complaining about zip a
being the wrong type of function.
It then separately complains that the second argument of the $
operator is also the wrong type to be passed as an argument to the whole function (of which zip a
is a small part), but that's quite a separate issue from the other error.
What Haskell is doing during type checking is looking at every expression (including sub-expressions, at every level of nesting), and comparing:
- The type the expression must have, in order to fit into its context (it calls this the "expected type")
- The type the expression would have based on its components (it calls this the "actual type")
You can think of the process in this example roughly as follows:
sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $ b
must result inDouble
, because of the type signature forpoly
- The first sub-expression is
$
applied tosum . map (\(ai, bi) -> ai * (x ** bi)) . zip a
$
has type(a -> b) -> a -> b
(actual type)1- We know that
b
above must beDouble
by the final expected return type ofpoly
, so$
should be something of the form(a -> Double) -> a > Double
(expected type) - Expected and actual types of
$
unify with no problems
- Now we know the expected type of
sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a
is something of the forma -> Double
. Lets check its actual type:- The first sub-expression in that composition chain is
.
applied tosum
((sum .)
in operator-section notation, or(.) sum
in prefix notation):.
has type(b -> c) -> (a -> b) -> a -> c
; its expected type in this position is something of the form(b -> Double) -> (a -> b) -> a -> Double
sum
has type(Foldable t, Num a) => t a -> a
; its expected type in this position is something of the formb -> Double
(needsNum Double
: ✔ )- So
(sum .)
has typeFoldable t => (a -> t Double) -> a -> Double
- The next sub-expression in the composition chain is
(sum .)
applied tomap (\(ai, bi) -> ai * (x ** bi)) . zip a
map (\(ai, bi) -> ai * (x ** bi)) . zip a
is expected to fitFoldable t => a -> t Double
. Lets check its actual type:- The first sub expression of that is
.
applied tomap (\(ai, bi) -> ai * (x ** bi))
.
has type(b -> c) -> (a -> b) -> a -> c
; its expected type in this position is something of the formFoldable t => (b -> t Double) -> (a -> b) -> a -> t Double
- So
map (\(ai, bi) -> ai * (x ** bi))
is expected to fitb -> t Double
- Skipping over the details,
map (\(ai, bi) -> ai * (x ** bi))
actually has type[(Double, Double)] -> [Double]
(becausex
is known to have typeDouble
from the signature ofpoly
). - This fits the expected type
b -> t Double
, and informs us thatb
is actually[(Double, Double)]
andt
is actually[]
(needsFoldable []
: ✔ )
- The first sub expression of that is
- So now we know that the actual type of
.
applied tomap (\(ai, bi) -> ai * (x ** bi))
is(a -> [(Double, Double)]) -> [Double]
, which means the second argument of the.
, which iszip a
, is expected to be of the forma -> [(Double, Double)]
. Lets check its actual type:zip
is of type[a] -> [b] -> [(a, b)]
a
is of type[Int]
from the type signature ofpoly
- So
zip a
has a type like[b] -> [(Int, b)]
. Trying to unify the expected and actual type forces us to instantiateb
to beDouble
, leaving the actual type ofzip a
being[Double] -> [(Int, Double)]
. But now there are no more type variables to instantiate. This is the first place we've found where the actual type doesn't match the expected type. So we emit a type error. In reporting the type error, we keep the fact thatb
was instantiated toDouble
, because nothing was wrong with that. So the expected type is shown as[Double] -> [(Double, Double)]
and the actual type is shown as[Double] -> [(Int, Double)]
- There's not much point drilling down further into
zip a
, because there is no meaningful expected type for the sub-components, because we don't know whether the issue we just reported was that the expected type is wrong or that the actual type was wrong (we just know that they can't be both right). We cannot say whether the problem is thatzip
doesn't fit[Int] -> [Double] -> [(Double, Double])
, or thata
doesn't fit[Double]
, or whetherzip a
is actually correct and the problem is that the context was expecting[Double] -> [(Double, Double)]
.
- But going back out and pretending that
zip a
actually did fit its expected type, we establish thatmap (\(ai, bi) -> ai * (x ** bi)) . zip a
has "actual type"[Double] -> [Double]
, which does unify with our expected type ofFoldable t => a -> t Double
- And that means that
sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a
has actual type[Double] -> Double
, which does unify with our expected type ofa -> Double
(and we now know thata
isDouble
).
- The first sub-expression in that composition chain is
- Which finally allows us to get to the next top-level expression, which is
(sum . map (\(ai, bi) -> ai * (x ** bi)) . zip a $)
applied tob
.b
is expected to have type[Double]
b
actually has type[Int]
(by the signature forpoly
)- This is our second place where actual and expected type do not match, so we report the second type error.
1 But not its actual actual type. Saying $
is simply a function with type (a -> b) -> a -> b
is actually a simplification, because $
needs to support things like unlifted types, which ordinary type variables can't support. But I'm not going to get into that here. The simplification works 99% of the time.
You can see that there are a huge number of steps to follow in working out how the type system generates these errors. So I don't really find that's a helpful process to follow in trying to understand type errors.
The compiler pinpoints the exact expression its talking about: both in terms of the descent of the parse tree with all those "in the second argument of (.)
" lines, and (usually more helpfully) with the graphical indication using ^^^^
characters underneath.
So step one is to think about "why would that expression be expected to have that type", looking at the surroundings. In this case it's reasonably clear why zip a
should have type [Double] -> [(Double, Double)]
; the result is feeding into mathematical operations that eventually produce Double
, so both elements of the tuples in the list have to be Double
, and the parameter of zip a
must also be [Double]
.
Step 2 is to think about "why would that expression actually have that type". Again, that's even more obvious. If a :: [Int]
, then there's no way that zip a
can result in something fitting _ -> [(Double, _)]
.
The finicky details the compiler goes through to verify everything else in the context leading up to these errors is mostly irrelevant; it effectively told you that was all fine (by not emitting any type errors there).
It's also irrelevant why it discovers zip a
first and not b
, or why it complains about zip a
being a function that results in [(Int, Double)]
instead of complaining about a
being of type [Int]
. Fundamentally it's just going to find a place where the expected and actual type are inconsistent, without any way to tell which one is correct (often neither of them are).
These things are understandable, and they become reasonably intuitive as you work with the compiler for longer, but these facts very rarely actually help you understand and fix the error. Just pick the first error it reports, focus on the expression it's talking about, think about why the context would cause it to have the reported "expected type", and why the sub-parts of the expression would cause it to have the reported "actual type".
Contrary to GHC's reputation for inscrutable error messages, I actually find them to be much higher quality that those I typically get when working with other languages. When you aren't familiar with them they contain a lot of information in a new format, and so they're confusing. But once you are familiar with them they are actually very good.
In fact, this particular error message is exactly along the lines of the function foo expects an argument of type int, but received string
that you were expecting! It's just that the "function foo" is the .
operator (which you've used twice on the same line so it identifies exactly which one it's talking about) and the argument it's expecting is another function with a complex type. The only reason it looks more complicated than the type of error message you compare it to is that it splits the expected/actual part onto two lines for readability (and points out exactly which part of those two types doesn't match!) and gives you a lot of detail about exactly which sub-expression contains the error, instead of just saying line 11: function (.) expects an argument of type [Double] -> [(Double, Double)], but received [Double] -> [(Int, Double)]
.