A “truly” generic function in Haskell

Question

Suppose I have a compound data type -

data M o = M (String,o)

Now, I can define a function that works for ALL M irrespective of o. For example -

f :: M o -> M o
f (M (s,o)) = M (s++"!", o)

However, f is not really as general as I'd like it to be. In particular, using f in an expression fixes the type of o so I cannot use f again with a different type of o. For example the following does not typecheck -

p f = undefined where
  m1 = M ("1", ())
  m2 = M ("2", True)
  m1' = f m1
  m2' = f m2

It produces the error - Couldn't match expected type 'Bool' with actual type '()'

Surprisingly, if I don't provide f as an argument and instead simply use the global definition of f then it compiles and works fine! i.e. this compiles -

p = undefined where
  m1 = M ("1", ())
  m2 = M ("2", True)
  m1' = f m1
  m2' = f m2

Is there a particular reason for this? How can I work around this problem i.e. define a function f that can be applied to all (M o), even when the o varies within the same expression? I'm guessing existential types come into play here but I just can't figure out how.

Answer 1

The problem is that the compiler cannot infer the type of p properly. You'll have to give it a type signature:

p :: (forall o. M o -> M o) -> a

This is a rank 2 type, so you'll need a language extension:

{-# LANGUAGE Rank2Types #-}

or

{-# LANGUAGE RankNTypes #-}

Read more about it here: http://www.haskell.org/haskellwiki/Rank-N_types

Answer 2

Is there a particular reason for this?

Indeed, there is one. To say it in one sentence: type inference will not work properly if one lifts the restriction of the HM system that lambda arguments must be monomorphic.

Simon Peyton Jones has devised a type checker that extends HM and allows higher rank polymorphism. But in such cases, explicit type annotations are required. See Sjoerds Answer.

Answer 3

The f in the scope of the function p f is not the same as the top level function f. It is whatever function is given as the argument when p is called. Since you didn't give p a type signature, the compiler has to infer what f is from how you use it. Your first use implies that f :: M () -> M (), which means p :: (M () -> M ()) -> a. As someone else said, you have to give p an explicit signature using forall to do what you're trying to do.