On the other hand if types are annotated with the exceptions they
throw then they become just another return value and become pure.
Same input, same exception every time.

As far as Yotam Barnoy's goal is concerned, this isn't true. He wants to be able to use purity annotations for optimisation: a most typical optimisation which is valid only for pure functions is to rewrite map f (map g l) into map (f∘g) l. This optimisation, as it happens, is not valid with exception throwing functions as it may very well throw a different exception.