Why does this function not work with typecheck?

Question

During a lecture on functional programming, we saw the following Haskell function:

f :: Bool -> Int -> (a -> Int) -> Int fxyz = if x then y + y else (zx) + (zy) 

This function is not expected to be tested by typecheck. However, the reason for this is not explained. When testing in GHCI, I got the following result:

  Prelude>: l test [1 of 1] Compiling Main (test.hs,
 interpreted)

 test.hs: 2: 35:
     Couldn't match expected type `a 'with actual type` Bool'
       `a 'is a rigid type variable bound by
           the type signature for f :: Bool -> Int -> (a -> Int) -> Int
           at test.hs: 1: 6
     Relevant bindings include
       z :: a -> Int (bound at test.hs: 2: 7)
       f :: Bool -> Int -> (a -> Int) -> Int (bound at test.hs: 2: 1)
     In the first argument of `z ', namely` x'
     In the first argument of `(+) ', namely` (zx)' Failed, modules loaded: none.

Why is this happening?

Answer 1

 f :: Bool -> Int -> (a -> Int) -> Int fxyz = if x then y + y else (zx) + (zy) 

A type signature states that our function z is polymorphic in its first argument. It takes a value of any type a and returns Int . However, the scope of a variable of type a also means that it must be of the same type of a for all purposes. a cannot be created for different types on the same site. This is a "rank 1 polymorphism."

You can read the type as really:

 f :: forall a. Bool -> Int -> (a -> Int) -> Int 

So:

 z (x :: Bool) + z (y :: Int) 

unacceptable, since a limited to two different independent types.

An extension of the language allows us to change the region a so that it can be created into a polymorphic variable, i.e. contain different types on the same site of use, including having polymorphic types of functions:

 Prelude> :set -XRankNTypes Prelude> let f :: Bool -> Int -> (forall a . a -> Int) -> Int fxyz = if x then y + y else (zx) + (zy) 

Type a now has no global scope, and individual instances may vary. This allows us to write a "more polymorphic" function f and use it:

 Prelude> f True 7 (const 1) 14 

So, as a cool polymorphism of a higher rank. More code reuse.

Answer 2

This is simply not how simple parametric polymorphism works. The function z polymorphic in the signature of the function, but in the body its only monomorphism.

When checking type definitions, the checking type introduces a monomorphic type for a variable of type a to be used throughout the function definition. However, your f trying to call z with two different types, and thus a type check displays two conflicting types for a .

Answer 3

Even

 f :: Bool -> Int -> (a -> Int) -> Int fxyz = if x then y + y else (zy) + (zy) 

there will be no typecheck (as mentioned in the comments) and will generate the same error, because Haskell indicates the least common types of expressions, and your type is more general than the intended one. Like the "Gentle Introduction to Haskell," adds

The basic type of an expression or function is the least general type, which intuitively "contains all instances of the expression."

If you specify the type explicitly, Haskell assumes that you did this for some reason, and insists that the inferred type matches this type.

For the expression above, the type deduced is (Num t) => Bool -> t -> (t -> t) -> t , so when matching the types, it sees that you gave Int for y , and the type z becomes (Int -> Int) Which is less common than (a -> Int) . But you insisted on having a (not Int ) - a hard-type variable. In other words, your function f can only accept functions of type Int -> Int , but you insist that any function :: a -> Int , including :: String -> Int , etc. can be provided to it. (As @augustsson points out in the comments), your declared type is too wide.

Similarly, if you had only one (zx) , it would correspond to the given type x and come to a narrower than the declared type (Bool -> Int) for the function z . And again complain about a hard variable of type.

In fact, you declared type (Num t) => Bool -> t -> (t1 -> t) -> t , but actually it is (Num t) => Bool -> t -> (t -> t) -> t . This is a different type.