What does it mean that the semantics (of Haskell) are affected by the inferred types (of return type polymorphism)?

Question

Here the commentator writes:

Finally, given enough macro magic this could be done... but likely for now less effort than implementing a Haskell-style type system atop Clojure. Typed Clojure could be a great model for this except it's been explicitly designed so that the semantics of Clojure cannot be affected by the inferred types. This is exactly what happens in return type polymorphism and so it's explicitly impossible in Typed Clojure.

My question is - What does it mean that the semantics (of Haskell) are affected by the inferred types (of return type polymorphism)?

Answer 1

Consider the read function, which has an (ad-hoc) polymorphic return value:

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

The implementation isn't so important. The only important part is that the implementation depends on the instance of Read chosen at compile time, and that inference can result in different types being chosen for the same call to read.

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

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

There's a call to read with the same argument twice. Haskell requires referential transparency, so it has to result in the same thing both times, right? Well, not quite. The inferred return type matters. In the print line, the inferred return type is Int. In the putStrLn line, the inferred return type is String. And because it's ad-hoc polymorphic, the semantics change with with the type variable.

The print line will print out 16. The putStrLn line will crash, because "11" is not an input that read will successfully decode into a String.

And because the type variable appears only in the return type, there's no value of that type at the time the function is called. There's no way to dispatch on a value's type at runtime to figure out what instance of Read to use. The only way to figure it out is by knowing the type at compile time. So Typed Clojure can't do this - it means semantics depend on compile-time types.

Edits to address comment

I have no idea if it's supposed to impress you. But since your statement (2) is wrong in every way possible, it indicates a clear lack of foundations for even understanding this example. I think I have to go all the way back to what a type variable means in Haskell to explain this.

A type variable in Haskell represents an unknown but concrete type, chosen by the caller. The type Read a => String -> a does not mean the function chooses a type for its return value based on its input. It means that the function chooses how it will work based on the type it outputs.

Perhaps read was a bad example, in that its varying behaviors only look particularly different when it throws an exception due to bad input. And it's really easy for people with no experience with Haskell's type system to conflate that with something like a runtime casting exception, even though it's entirely different.

Your statement (2) is entirely wrong. The program does not crash because read returns an Int where the code expected a String, and something like a ClassCastException happens. The program crashes because read chose a parser for parsing String literals based on its return type at compile time, but the input it was given was not a valid String literal. (In contrast, "\"11\"" is a valid String literal because it is quoted.)

The bolded part is the important part. The read function chooses what parser it's going to use at compile time based on the return type. That is both an extremely powerful technique, and something you cannot do with Typed Clojure.

Answer 2

One way to see this distinction is to examine System F. It's pretty similar to Haskell except that all polymorphism is explicitly introduced using "type lambdas". The typical notation is that type lambdas appear in type declarations as "forall" quantification (I'll write \/) and in values as "big lambdas" (I'll write /\).

So, for instance, id becomes

id :: \/ a . a -> a
id = /\ type -> \x -> x

So we have to explicitly pass the type instantiating the variable a in order to use id. You might see this used as

> id Int 3
3 :: Int

---

So, what does this have to do with return type polymorphism? Well, Haskell's type inferencer (the Hindley-Milner) system can be thought of as essentially living atop System F, automatically piping around the types. To do this it restricts a lot of the flexibility of System F, but we'll ignore that for now.

All you have to keep in mind is that the type inferencer figures out what the type variables ought to be instantiated as, all before runtime. Or, more clearly, at runtime all type lambdas are eliminated. This is what allows the compile-time/run-time phase distinction, what allows type erasure.

---

Haskell extends Hindley-Milner to allow a kind of bounded polymorphism. The type

\/ a . C a => a

says that the type lambda can be fulfilled only by types which are bounded by C. Haskell then solves equations about these bounds to determine the right types to insert wherever.

This is where we get return-type polymorphism. When we're inferencing the type which must have been passed to a particular type lambda we use information about both the inputs and outputs of a function

f :: a -> b
e :: a

f e :: b

if the return type of a function can constrain the type variables then it will. This will let the inferencer pick the right System F variant. Then, at runtime all of the type lambdas are gone and only the exact, type-free code which matches the return type demanded remains.