Why is this (unexpected) type returned by a higher order function?

Question

Confused by haskell types [*]

I am beginning to learn haskell and am confused by the result of haskells type inference (see example below). Unfortunately I am not fluent enough in haskell to formulate the real question, so I have to work by example.

[*] As soon as I know the real question, I'll update the caption..

My goal

I am following the Get programming with haskell book. In lesson 10 a way to 'hold state' is shown:

-- The result of calling robot (`r`) is a function that takes 
-- another function (`message` as argument). The parameters 
-- passed to the initial call to `robot` are treated 
-- as state and can be passed to `message`.
-- 
robot name health attack = \message -> message name health attack

getName r = r (\name _ _ -> name)

klaus = robot "Klaus" 50 5

*Main> getName klaus
"Klaus"

I think I understood the gist of it and tried to create a little robot fight. In the end I wanted something like this:

klaus = robot "Klaus" 50 5
peter = robot "Peter" 50 5

victor = fight klaus peter

getName victor
-- should be "Klaus"

My robots

This is the implementation I wrote:

robot name health attack = \message -> message name health attack

isAlive r = r (\_ health _ -> health > 0)

fight attacker defender = if isAlive attacker then
                             attacker
                          else
                             defender



printRobot r = r (\name health  attack -> "Name: " ++ (show name) ++", health: " ++ (show health) ++ ", attack: " ++ (show attack))

klaus = robot "Klaus" 50 5
peter = robot "Peter" 60 7

Experimenting in ghci

The code loads in ghci (:l robots.hs). When I experiment with my code I found out that things don't exactly work out as planned: The type system and I seem to have different ideas of what the resulting types look like.

Please point out where my reasoning is wrong and help me understand the error of my ways :-)

--
-- in ghci
--

*Main> :t klaus
-- I understood: 
-- klaus is a function. I have to pass a function that
-- takes name, health, and attack as parameters and 
-- returns something of type "t". 
--
-- A result of same type "t" is then returned by calling klaus
klaus :: ([Char] -> Integer -> Integer -> t) -> t

-- check the "isAlive" function:
-- As expected, it returns a Bool
*Main> :t isAlive klaus
isAlive klaus :: Bool

-- This is also expected as klaus has health > 0
*Main> isAlive klaus
True

-- Inspecting the type of `isAlive` confuses me:
--
-- I do understand:
--
-- The first parameter is my "robot". It has to accept a function
-- that returns a boolean (basically the isAlive logic):
--
-- (t1 -> a -> t -> Bool) 
-- - t1: name, ignored
-- - a: health, needs to be a comparable number 
-- - t: attack value, ignored
-- - returns boolean value if the health is >0
--
-- What I do NOT understand is, why doesn't it have the following type
-- isAlive :: (Ord a, Num a) => (t1 -> a -> t -> Bool) -> Bool
*Main> :t isAlive
isAlive :: (Ord a, Num a) => ((t1 -> a -> t -> Bool) -> t2) -> t2

-- The signature of `isAlive` bites me in my simplified 
-- fight club:
-- If the attacker is alive,  the attacker wins, else 
-- the defender wins:
fight attacker defender = if isAlive attacker then
                 attacker
              else
                 defender

-- I would expect the "fight" function to return a "robot".
-- But it does not:
*Main> victor = fight klaus peter
*Main> :t victor
victor :: ([Char] -> Integer -> Integer -> Bool) -> Bool

*Main> printRobot klaus
"Name: \"Klaus\", health: 50, attack: 5"
*Main> printRobot peter
"Name: \"Peter\", health: 60, attack: 7"
*Main> printRobot victor 

<interactive>:25:12: error:
    • Couldn't match type ‘[Char]’ with ‘Bool’
      Expected type: ([Char] -> Integer -> Integer -> [Char]) -> Bool
        Actual type: ([Char] -> Integer -> Integer -> Bool) -> Bool
    • In the first argument of ‘printRobot’, namely ‘victor’
      In the expression: printRobot victor
      In an equation for ‘it’: it = printRobot victor

The questions

• Why is the signature of isAlive not (t1 -> a -> t -> Bool) -> Bool?
• What is wrong with my fight function?

What I have learned so far

With my current understanding I cannot fix the problem, but now (thanks to the great answer of @chi) I can understand the problem.

For all the other beginners that stumble into the same pitfall, here is my reasoning with a simplified version of the problem:

• I build a closure holding two strings s1, s2 and an int i1 via buildSSIclosure. By "sending a message" (passing a function) into the closure I can access the "state" of the closure.
• I can write simple accessors getS1, getS2, and getI1
• I want to write a function that takes an ssiClosure and gets both the Int, and a [Char] property via the accessors.

-- IMPORTANT: the return value `t` is not bound to a specific type
buildSSIclosure :: [Char] -> [Char] -> Int -> ([Char] -> [Char] -> Int -> t) -> t
buildSSIclosure s1 s2 i1 = (\message -> message s1 s2 i1)

The definition of buildSSIclosure had t unbound. When any of the accessors is used the t of the ssiClosure instance is bound to a type:

getS1 :: (([Char] -> [Char] -> Int -> [Char]) -> [Char]) -> [Char]
getS2 :: (([Char] -> [Char] -> Int -> [Char]) -> [Char]) -> [Char]
getI1 :: (([Char] -> [Char] -> Int -> Int) -> Int) -> Int

-- `t` is bound to [Char]
getS1 ssiClosure = ssiClosure (\ s1 _ _ -> s1)

-- `t` is bound to [Char]
getS2 ssiClosure = ssiClosure (\ _ s2 _ -> s2)

-- `t` is bound to int
getI1 ssiClosure = ssiClosure (\ _ _ i1 -> i1)

I directly access both parameters of the call to the lambda function This works and will bind t to [Char]:

getS1I1_direct ssiClosure = ssiClosure (\ s1 _ i1 -> s1 ++ ", " ++ show i1)

Call two string accessors

I can access both S1 and S2 via the accessors. This works because both getS1, and getS2 bind t from ssiClosure to [Char]:

getS1S2_indirect ssiClosure = show (getS1 ssiClosure) ++ ", " ++ show(getS2 ssiClosure)

Access Char and Int

The next step is to access the int, and the string properties. That will not even compile!

Here is my understanding:

• Calling getS1 needs t from the closure to be bound to [Char]
• Calling getI1 needs t from the closure to be bound to Int

It cannot be bound to both, so the compiler tells me so:

getS1I1_indirect ssiClosure = show(getS1 ssiClosure) ++ ", "  ++ show(getI1 ssiClosure)

    • Couldn't match type ‘[Char]’ with ‘Int’
      Expected type: ([Char] -> [Char] -> Int -> Int) -> Int
        Actual type: ([Char] -> [Char] -> Int -> [Char]) -> [Char]
    • In the first argument of ‘getI1’, namely ‘ssiClosure’
      In the first argument of ‘show’, namely ‘(getI1 ssiClosure)’
      In the second argument of ‘(++)’, namely ‘show (getI1 ssiClosure)’

I still don't have to skill to identify the problem by looking at the error. But there is hope ;-)

Answer 1

Why is the signature of isAlive not (t1 -> a -> t -> Bool) -> Bool?

isAlive r = r (\_ health _ -> health > 0)

Let's start form the lambda. I think you can see that

(\_ health _ -> health > 0) :: a -> b -> c -> Bool

where b must be both of class Ord (for >) and Num (for 0)

Since the argument r takes as input the lambda, it must be a function taking as input the lambda:

r :: (a -> b -> c -> Bool) -> result

Finally, isAlive takes r as argument, and returns the same result as r. Hence:

isAlive :: ((a -> b -> c -> Bool) -> result) -> result

Adding the constraints and renaming the type variables a bit, we get GHCi's type:

isAlive :: (Ord a, Num a) => ((t1 -> a -> t -> Bool) -> t2) -> t2

Note that this type is more general than this:

isAlive :: (Ord a, Num a) => ((t1 -> a -> t -> Bool) -> Bool) -> Bool

which roughly means "give me a Bool-generating robot, and I'll give you a Bool".

What is wrong with my fight function?

fight attacker defender = if isAlive attacker then
                 attacker
              else
                 defender

This is tricky. The code above calls isAlive attacker and that forces attacker to have type (a -> b -> c -> Bool) -> result. Then, result must be Bool because it is used in the if. Moreover, this makes defender to have the same type as attacker since both branches of if then else must return values of the same type.

Hence, the output of fight must be a "Bool-generating robot", i.e. a robot which is no longer able to generate anything else.

This can be fixed using rank-2 types, but if you are a beginner I am not recommending to try this right now. This exercise looks quite advanced for a beginner, since there are a lot of lambdas being passed around.

More technically, you are passing Church-encoded tuples everywhere, and that will fully work only with rank-2 polymorphism. Passing first-order tuples would be much simpler.

Anyway, here's a possible fix. This prints Klaus as the winner.

{-# LANGUAGE Rank2Types #-}

isAlive :: (Ord h, Num h) => ((n -> h -> a -> Bool) -> Bool) -> Bool
isAlive r = r (\_ health _ -> health > 0)

-- A rank-2 polymorphic robot, isomorphic to (n, h, a)
type Robot n h a = forall result . (n -> h -> a -> result) -> result

fight :: (Ord h, Num h) => Robot n h a -> Robot n h a -> Robot n h a
fight attacker defender = if isAlive attacker
   then attacker
   else defender

robot :: n -> h -> a -> Robot n h a
robot name health attack = \message -> message name health attack

printRobot :: (Show n, Show h, Show a) => ((n -> h -> a -> String) -> String) -> String
printRobot r = r (\name health  attack -> 
   "Name: " ++ show name ++
   ", health: " ++ show health ++
   ", attack: " ++ show attack)

klaus, peter :: Robot String Int Int
klaus = robot "Klaus" 50 5
peter = robot "Peter" 60 7

main :: IO ()
main = do
   let victor = fight klaus peter
   putStrLn (printRobot victor)

A final note

I would recommend you add types to each one of your top-level functions. While Haskell can infer those, it is very convenient for the programmer to have types at hand. Further, if you write the type you intend to have, GHC will check it. It often happens that GHC infers a type which was not intended by the programmer, making the code looks fine when it is not. This usually then causes puzzling type errors later on in the program, when the inferred type mismatches with the rest of the code.