Why do Haskell inferred types in return type polymorphism lead to runtime errors?

Question

The reason I'd choose to use Haskell is because of its rich type system. This gives me more information at compile-time about my program, helping me have confidence that it is sound.

In addition, it would appear that Haskell is an optimal language in which to approach the expression problem, as Haskell typeclasses can dispatch on return type. (In contrast to Clojure protocols - which can only dispatch on first argument).

When I explore a Haskell polymorphic return value function like read:

read :: (Read a) => String -> a

with the following program:

addFive :: Int -> Int
addFive x = x + 5

main :: IO ()
main = do
    print (addFive (read "11"))
    putStrLn (read "11")

I get the following result:

Runtime error
...
prog: Prelude.read: no parse

So I appear to be getting a runtime error in a language with a superior type system.

Contrast this with the equivalent code in Clojure:

(defn add-five [x] (+ 5 x))

(println (add-five (read-string "11")))
(println (read-string "11"))

This gives the following result:

16
11

My question is Why do Haskell inferred types in return type polymorphism lead to runtime errors? Shouldn't it pick them up at compile-time?

Answer 1

A part of the issue here is that in Haskell one can define partial functions, i.e., functions which may fail on certain inputs. Examples are read, head, tail. Non-exhaustive pattern matching is the common cause of this partiality, others including error, undefined, and infinite recursion (even if in this case you do not get a runtime error, obviously).

In particular, read is a bit nasty since it requires you to ensure that the string can be parsed. This is usually harder than ensuring that a list is non empty, for instance. One should use a safer variant such as

readMaybe :: Read a => String -> Maybe a

main = do
  print $ readMaybe "11" :: Maybe Int     -- prints Just 11
  print $ readMaybe "11" :: Maybe String  -- prints Nothing

Another part of the issue is that polymorphic values (such as read "11") are actually functions in disguise, since they depend on the type at which they are evaluated, as seen in the example above. The monomorphism restriction is an attempt to make them behave more as non-functions: it forces the compiler to find a single type for all the uses of the polymorphic value. If this is possible, the polymorphic value is evaluated only at that type, and the result can be shared in all the uses. Otherwise, you get a type error, even if the code would have been typeable without the restriction.

For example, the following code

main = do
  let x = readMaybe "11"
  print $ x :: Maybe Int
  print $ x :: Maybe Int

parses 11 once if the monomorphism restriction is on, and twice if it is off (unless the compiler is smart enough to do some optimization). By comparison,

main = do
  let x = readMaybe "11"
  print $ x :: Maybe Int
  print $ x :: Maybe String

raises a compile-time type error if the monomorphism restriction is on, and compiles and runs just fine if it is off (printing "Just 11" and "Nothing").

So, there is no clear winner between enabling and disabling the restriction.

Answer 2

The type of read is

(Read a) => String -> a

which implies it (compiler or interpreter, actually) will choose its return type according to the requirement of context.

Therefore, in addFive (read "11"), because addFive requires a Int, the type of read chosen by compiler will be String -> Int; in putStrLn (read "11"), it will be String->String because putStrLn requires a String.

And this choice happens at compile time, which means after compilation, your program sort of equals

main = do
    print (addFive (readInt "11"))
    putStrLn (readString "11")

But this readString cannot parse its argument "11" as a string, so it crash at run time.

The fix of this problem is simple:

main = do
    print (addFive (read "11"))
    putStrLn (read "\"11\"")

Answer 3

That runtime error has nothing to do with polymorphism, and everything to do with the fact that the string "11" can't be parsed as a list of characters by the read function.

Here are things that work. Note that "11" can, at runtime, be parsed as an Int and "\"Some More String\"" can, at runtime, be parsed as a string.

print $ 5 + read "11"
print $ "Some string" ++ read "\"Some More String\""

Here are some things that don't work. They don't work because "Not an integer" can not be parsed as an Int and "11" can't be parsed as a string.

print $ 5 + read "Not an integer"
print $ "Some string" ++ read "11"

As was pointed out in the answer to your previous question, the type information has already been inferred at compile time. The read functions have already been selected. Imagine if we had two functions readInt :: String -> Int and readString :: String -> String that were provided for the read function for the Read instances for Int and String respectively. The compiler has already, at compile time, replaced the occurrences of read with the original respective functions:

print $ 5 + readInt "Not an integer"
print $ "Some string" ++ readString "11"

This must have happened at compile time precisely because type information is eliminated at compile time, as was explained in the answer to your previous question.