How to understand Haskell compiler messages_问答_开发者

Good day.

Here is simple "guess number" snippet and it contains single error, but compiler makes it really hard to undertstand what is wrong:

import System.Random
import Control.Monad
import Control.Monad.Cont

main = do
  rn <- randomRIO (1,10) :: IO Int
  runContT (callCC $ \k -> forever $ do
    lift $ putStr "Your number:"
    n <- lift (fmap read getLine)
    when (n == rn) $ k
    lift $ putStrLn $ if (n > rn) 
                      the开发者_开发知识库n "Too much" 
                      else "Too little") (return)
  putStrLn $ "Good guess! " ++ (show rn)

GHC gives the error:

> simple.hs:11:21:
>     Couldn't match expected type `()' against inferred type `m b'
>       Expected type: a -> ()
>       Inferred type: a -> m b
>     In the second argument of `($)', namely `k'
>     In a stmt of a 'do' expression: when (n == rn) $ k

And it making me really confused, it tells that something expected type '()', but how to spot who is this "something" ? Is it "k" ? don't seem to be so. It look saner if we exchange expected and inferred, but how it look now, it is very confusing. My question is: how to spot cause and fix this error ?

To understand these types, it is good to look a the surrounding functions.

The error mentions the variable k, which first appears in the expression callCC $ \k -> forever .... We can get the type of k by looking at the type of callCC:

callCC :: MonadCont m => ((a -> m b) -> m a) -> m a

From that, we can see that k has the type a -> m b. Note that as b isn't used anywhere else in that function, the type of it doesn't matter and will be determined by the context the the function is used in.

k is being used in the when expression, after the $ (which isn't actually needed). The type of when is:

 when :: Monad m => Bool -> m () -> m ()

Note the second argument expects a m (), but you are passing in k, which has type a -> m b (since b doesn't matter it can match (). So obviously some argument needs to be given to k. To figure out what a is, we look back at the definition of callCC. That arg is the value forever $ do ... in your program.

Looking at the type of forever:

forever :: Monad m => m a -> m b

It takes one monadic computation m a, and as a result returns another monadic computation m b. Note how b doesn't appear in the arguments of forever. This means that the type is determined by the context in which it is called (like read "3" can be of type Double or Int depending on the expression it is in). This is determined by runContT:

runContT :: ContT r m a -> (a -> m r) -> m r

If you match up the type variables from runContT, callCC and forever, you will note that the b in forever corresponds to the a in runContT. The a is used in the second argument to runContT, which in your program is return. return has type a -> m a, so the type of a is the same as r in your program. r appears in the output m r.

The runContT expression is in a do context, without any bindings (<-). So your code is equivalent to this:

main = do
  rn <- randomRIO (1,10) :: IO Int
  runContT (callCC ....) (return) >> (putStrLn $ "Good guess! " ++ (show rn))

The mystery will finally be solved by looking at the type of >>:

(>>) :: Monad m => m a -> m b -> m b

>> discards the value of the first monadic computation passed to it (which was the runContT expression). So the value that computation returns doesn't actually matter (note how a doesn't appears in the result of the >> function). If you follow the consequence of this back through this explanation, you will realize that the variable passed to k actually doesn't matter! If you pass anything to it, the function will work correctly:

import System.Random
import Control.Monad
import Control.Monad.Cont

main = do
  rn <- randomRIO (1,10) :: IO Int
  runContT (callCC $ \k -> forever $ do
    lift $ putStr "Your number:"
    n <- lift (fmap read getLine)
    when (n == rn) $ k (Just ("Seriously anything works here", 42, [42..]))
    lift $ putStrLn $ if (n > rn) 
                      then "Too much" 
                      else "Too little") (return)
  putStrLn $ "Good guess! " ++ (show rn)

So that was a really hard example and I understand why you didn't follow it. You do get better with experience though. Also, the continuation monad is pretty advanced and complicated haskell.

The key things to look for in GHC warnings messages are:

Type you have; type it needs to be

Couldn't match expected type `()' against inferred type `m b'

so you have something of type (), in a monadic setting m b.

What expression is at fault

In the second argument of `($)', namely `k'

So k has the wrong type.

Line numbers

simple.hs:11:21

on line 11.

Don't get too hung up on "expected" vs. "inferred". Which is which is not always obvious and less often relevant; the important thing is that the type checker has conflicting information about the type of some term. The most common case is that one type is expected by the context (e.g., applying a function that takes an argument of a specific type) while a different type is inferred for the term.

Now, for the error you got:

Couldn't match expected type `()' against inferred type `m b'

This means that the conflicting types are () and m b. Note that these aren't necessarily the full types of any actual expression; just the part that's conflicting.

Expected type: a -> ()
Inferred type: a -> m b

Here we have the two actual types. The a -> parts don't conflict, so weren't mentioned above.

In the second argument of `($)', namely `k'

This tells us the context where the conflict was found, and gives the expression whose type is at issue, namely k.

The inferred type here is the type it "already knows" for k. Where does that come from? k is bound as the argument to a lambda passed to callCC, which has the type ((a -> m b) -> m a) -> m a, so that's the inferred type.

The expected type here is the second argument to when, which has type Bool -> m () -> m (), which gives us m (). Where does a -> () come from, though? We get that because a -> _ is equivalent to (->) a, which unifies with the type variable m in when's type signature.

Obviously that's not what you want the types to be, but you asked how to interpret the error so I'll leave it at that.

Expected type means what you should have in that spot. In you case, we have when :: (Monad m) => Bool -> m () -> m (). The compiler thus deduces, that the k in when (n == rn) $ k ought to be of type a -> ().

Inferred type means the actual type the compiler deduced for a variable. In your case, we have callCC :: (MonadCont m) => ((a -> m b) -> m a) -> m a. This means the anonymous function it receives is of type (a -> m b) -> m a. Since k is the fist argument of this function, the compiler concludes that k seems to be of type a -> m b.

Since the two types don't match, you get an error.

The error in this case is that you're not giving the continuation k the value to return from the callCC.

Changing