catch violates the semantic approximation order?

Question

The semantic approximation order states that if a function f is defined when one its arguments is not, then f is constant in that argument (it doesn't use it). But consider this function,

import Control.Exception

handleAll :: SomeException -> IO ()
handleAll e = putStrLn "caught"

f :: String -> IO ()
f x = catch (putStrLn x) handleAll

f undefined displays caught in GHCi, so it looks defined. However f is not constant in its argument, because f "test" displays test.

Is there a mistake somewhere ?

Answer 1

To model exceptions and catch properly you need a richer denotational semantics for terms, that distinguishes exceptions from nontermination (and that distinguishes different exceptions from each other). See A semantics for imprecise exceptions (pdf) for the semantics that GHC implements.

Note that this has no effect on the denotational semantics of the "pure fragment" of Haskell, since you have no way to observe distinctions between IO a values in pure code (aside from bottom vs. not-bottom).

To clarify what I mean by the "pure fragment" of Haskell, imagine defining the IO type as

data IO a = MkIO

and catch as

catch a h = MkIO

Now there's no problem with your f, since both f undefined and f "test" are equal to MkIO. From the viewpoint of denotational semantics this corresponds to the interpretation

[[IO t]] = {⊥ < ⊤}

Since the only operations we can do with IO actions are seqing them and combining them into other IO actions, it's a perfectly consistent denotational semantics which does not compromise your ability to talk about the semantics of things like length :: [Bool] -> Integer. It just happens to be useless for understanding what happens when you execute an IO action. But if you wanted to treat that in a denotational semantics, you'd encounter many difficulties besides exceptions.