5

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

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

It is expected that this function will fail to typecheck. However, the reason why this happens was not explained. When trying it out in GHCI I got the following output:

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 `(z x)' Failed, modules loaded: none.

Why does this happen?

Improve this question
2
  • 2
    Suppose I call f like f True 3 (\n -> n+1). What would you expect to happen? Commented Sep 16, 2014 at 11:01
  • 3
    Remember that the type f :: Bool -> Int -> (a -> Int) -> Int means that the caller gets to pick the a. So it perfectly fine for the caller to choose a function with type String -> Int. Commented Sep 16, 2014 at 12:07

3 Answers 3

Reset to default
8 
f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

The type signature asserts that our function z is polymorphic in its first argument. It takes a value of any type a and returns an Int. However, the scoping of the type variable a also means that it must be the same type a at all uses. a cannot be instantiated to different types at the same use site. This is "rank 1 polymoprhism".

You can read the type as really:

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

So:

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

is invalid, as a is constrained to two different, independant types.

A language extension allows us to change the scope of a so that it can be instantiated to a polymorphic variable -- i.e. to hold different types at the same use site, including to have polymorphic function types:

Prelude> :set -XRankNTypes

Prelude> let f :: Bool -> Int -> (forall a . a -> Int) -> Int 
             f x y z = if x then y + y else (z x) + (z y)

Now the type a doesn't have global scope, and individual instantiations can vary. This lets us write the "more polymorphic" function f and use it:

Prelude> f True 7 (const 1)
14

So that's how cool higher rank polymorphism is. More code reuse.

Improve this answer
Sign up to request clarification or add additional context in comments.

5 Comments

I think this answer confuses a little, as it doesn't work even for this (z x) + (z x), where z is applied with the same type.
Hmm? f :: Bool -> Int -> (forall a . a -> Int) -> Int ; f x y z = if x then y + y else (z x) + (z x) is perfectly well-typed with rank N.
Typechecks well with rank N. But the statement a is constrained to two different, independent types. is a little confusing because even if a was constrained to a single type (z x + z x), it doesn't compile with the default Rank 1.
Or to be more clear, your answer suggests that because at the use site we have instantiated it with different types (Bool and Int) it doesn't work. But that is not the case, It doesn't work even if instantiated with a single type i.e (z x + z x).
Indeed, that sentence seems to imply that f x y z = if x then y + y then z y , applying z only to one argument, would pass type-checking with the original signature. This is not the case, though.
3

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

When type-checking the definition the type checker infers a monomorphic type for the type variable a to use throughout the definition of the function. Your f however tries to call z with two different types, and thus the type checker infers two conflicting types for a.

Improve this answer

Comments

2

Even 

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

wouldn't typecheck (as was pointed out in the comments), and generate the same error, because Haskell infers least general types for expressions, and your type is more general than the inferred. As "A Gentle Introduction to Haskell" puts it,

An expression's or function's principal type is the least general type that, intuitively, "contains all instances of the expression".

If you specify a type explicitly, Haskell assumes you did that for a reason, and insists on matching the inferred type to the given type.

For the expression above the inferred type is (Num t) => Bool -> t -> (t -> t) -> t, so when matching the types, it sees that you gave Int for y and the type of z becomes (Int -> Int). Which is less general than (a -> Int). But you insisted on having an a there (not an Int) — a rigid type variable. In other words, your function f can only accept functions of type Int -> Int, but you are insisting that it may be given any function :: a -> Int, including :: String -> Int etc. (as @augustsson points out in the comments). Your declared type is too broad.

Similarly, if you had just one (z x) it would match with the given type of x and arrive at the narrower than declared type (Bool -> Int) for the z function. And yet again complain about a rigid type variable.

In effect, you declared the type (Num t) => Bool -> t -> (t1 -> t) -> t but it really is (Num t) => Bool -> t -> (t -> t) -> t. It is a different type.

Improve this answer

2 Comments

I realized that and reverted back with a. :)
ah, just saw it. :) thanks for bringing up that example, that clarifies the issue.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.