When are type signatures necessary in Haskell?

Question

Many introductory texts will tell you that in Haskell type signatures are "almost always" optional. Can anybody quantify the "almost" part?

As far as I can tell, the only time you need an explicit signature is to disambiguate type classes. (The canonical example being read . show.) Are there other cases I haven't thought of, or is this it?

(I'm aware that if you go beyond Haskell 2010 there are plenty for exceptions. For example, GHC will never infer rank-N types. But rank-N types are a language extension, not part of the official standard [yet].)

Answer 1

Polymorphic recursion needs type annotations, in general.

f :: (a -> a) -> (a -> b) -> Int -> a -> b
f f1 g n x = 
    if n == (0 :: Int)
    then g x
    else f f1 (\z h -> g (h z)) (n-1) x f1

(Credit: Patrick Cousot)

Note how the recursive call looks badly typed (!): it calls itself with five arguments, despite f having only four! Then remember that b can be instantiated with c -> d, which causes an extra argument to appear.

The above contrived example computes

f f1 g n x = g (f1 (f1 (f1 ... (f1 x))))

where f1 is applied n times. Of course, there is a much simpler way to write an equivalent program.

Answer 2

Monomorphism restriction

If you have MonomorphismRestriction enabled, then sometimes you will need to add a type signature to get the most general type:

{-# LANGUAGE MonomorphismRestriction #-}
-- myPrint :: Show a => a -> IO ()
myPrint = print
main = do
  myPrint ()
  myPrint "hello"

This will fail because myPrint is monomorphic. You would need to uncomment the type signature to make it work, or disable MonomorphismRestriction.

Phantom constraints

When you put a polymorphic value with a constraint into a tuple, the tuple itself becomes polymorphic and has the same constraint:

myValue :: Read a => a
myValue = read "0"

myTuple :: Read a => (a, String)
myTuple = (myValue, "hello")

We know that the constraint affects the first part of the tuple but does not affect the second part. The type system doesn't know that, unfortunately, and will complain if you try to do this:

myString = snd myTuple

Even though intuitively one would expect myString to be just a String, the type checker needs to specialize the type variable a and figure out whether the constraint is actually satisfied. In order to make this expression work, one would need to annotate the type of either snd or myTuple:

myString = snd (myTuple :: ((), String))

Answer 3

In Haskell, as I'm sure you know, types are inferred. In other words, the compiler works out what type you want.

However, in Haskell, there are also polymorphic typeclasses, with functions that act in different ways depending on the return type. Here's an example of the Monad class, though I haven't defined everything:

class Monad m where
    return :: a -> m a
    (>>=) :: m a -> (a -> m b) -> m b
    fail :: String -> m a

We're given a lot of functions with just type signatures. Our job is to make instance declarations for different types that can be treated as Monads, like Maybe t or [t].

Have a look at this code - it won't work in the way we might expect:

return 7

That's a function from the Monad class, but because there's more than one Monad, we have to specify what return value/type we want, or it automatically becomes an IO Monad. So:

return 7 :: Maybe Int
-- Will return...
Just 7

return 6 :: [Int]
-- Will return...
[6]

This is because [t] and Maybe have both been defined in the Monad type class.

Here's another example, this time from the random typeclass. This code throws an error:

random (mkStdGen 100)

Because random returns something in the Random class, we'll have to define what type we want to return, with a StdGen object tupelo with whatever value we want:

random (mkStdGen 100) :: (Int, StdGen)
-- Returns...
(-3650871090684229393,693699796 2103410263)

random (mkStdGen 100) :: (Bool, StdGen)
-- Returns...
(True,4041414 40692)

This can all be found at learn you a Haskell online, though you'll have to do some long reading. This, I'm pretty much 100% certain, it the only time when types are necessary.