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.