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?

Will Ness
  • 70,110
  • 9
  • 98
  • 181
aochagavia
  • 5,887
  • 5
  • 34
  • 53
  • 2
    Suppose I call `f` like `f True 3 (\n -> n+1)`. What would you expect to happen? – Tom Ellis Sep 16 '14 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`. – augustss Sep 16 '14 at 12:07

3 Answers3

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.

Don Stewart
  • 137,316
  • 36
  • 365
  • 468
  • 2
    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. – Sibi Sep 16 '14 at 11:12
  • 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. – Don Stewart Sep 16 '14 at 11:15
  • 2
    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. – Sibi Sep 16 '14 at 11:19
  • 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)`. – Sibi Sep 16 '14 at 11:28
  • 2
    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. – chi Sep 16 '14 at 11:30
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.

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.

Will Ness
  • 70,110
  • 9
  • 98
  • 181