#1171: GHC doesn't respect the imprecise exceptions semantics
----------------------+-----------------------------------------------------
Reporter: neil | Owner:
Type: bug | Status: reopened
Priority: low | Milestone: _|_
Component: Compiler | Version: 6.6
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: cg059 | Architecture: Multiple
Os: Multiple |
----------------------+-----------------------------------------------------
Comment (by igloo):
The below is from e-mail and IRC conversations that happened in parallel
with this bug report.
I've editted things slightly to make them flow better, but hopefully
haven't changed any important meanings.
----
__I said:``__
In http://research.microsoft.com/~simonpj/Papers/imprecise-exn.htm
I think you claim in section 4.3, in the rationale for the Bad case,
that if we have
{{{
f x = case x of
True -> error "A"
False -> error "B"
}}}
then the call
{{{
f (error "X")
}}}
is allowed to raise B, as this permits transformations like
{{{
f' x = let b = error "B"
in b `seq` case x of
True -> error "A"
False -> b
}}}
which in turn is justified because the case expression is strict in
{{{
error "B"
}}}
(as well as every other expression).
However, the Ok case tells me that if I call
{{{
f True
}}}
then I can get the errors raised by the
{{{
True -> error "A"
}}}
branch only. Thus it must raise A. But with the above transformation f'
raises B.
I also think that this behaviour is very confusing to users; it makes
sense that
{{{
error "A" + error "B"
}}}
needs to evaluate both values, so throwing either exception is
reasonable, but in
{{{
f True
}}}
it is "obvious" that A is raised and B is not!
Traditionally, we would say that e is strict in x if
{{{
x = _|_ => e = _|_
}}}
However, with the set-based imprecise exceptions, in which we
distinguish between different bottoms, it seems to me that a better
definition would be that e is strict in x if
{{{
x = Bad xs => e = Bad ys and xs \subseteq ys
}}}
Thus, for example, a case can throw an exception if either the scrutinee
can or /all/ the branches can, i.e. in the Bad case in 4.3 we take the
big intersection rather than big union.
So we wouldn't be allowed to pull
{{{
error "B"
}}}
out of the above case, but we would still be able to translate
{{{
case x of
True -> y
False -> y
}}}
into
{{{
y `seq` case x of
True -> y
False -> y
}}}
I am also unconvinced by a non-terminating program being allowed to
throw anything it likes. It seems much nicer to permit it only to either
not terminate or to throw a special exception, here-on written N.
I haven't written a denotational semantics or anything, so perhaps this
would all unravel if I tried, but here are some example definitions
followed by what exceptions I think various expressions ought to be able
to throw; are there any obvious nasty corners I have left unexplored?:
{{{
f x = case x of
True -> error "A"
False -> error "B"
g x = case x of
True -> error "C"
False -> error "C"
h () () = ()
i = i
j = error "D" + j
-----
f True A
f (error "E") E
g True C
g (error "F") C or F
h (error "G") (error "H") G or H
i N or non-termination
j D, N or non-termination
}}}
I also haven't looked into the performance implications, although
personally I'd prefer a semantics that is more intuitive along with a
few more bang patterns sprinkled around.
----
__Simon PJ replied:``__
I think you are basically right here. Another way to say it is this. In
4.5 we
claim that GHC's transformations can reduce the set of possible exceptions
from
a term, but not increase it. But the (current) strictness analysis
transformation increases it. I agree that is undesirable.
As I say on the Trac, we could change this at the cost of making fewer
functions
strict. I can tell anyone how to do this, if you want. It would be good
to
measure the performance impact of doing so.
----
__Simon M__ has a memory that there is some problem, possibly related to
monotonicity, with only allowing non-terminating programs to either not
terminate or throw a special non-termination error, rather than allowing
them to behave like any bottom they wish as the imprecise exceptions paper
allows them to. However, he can't remember what the problem actually is;
if anyone can then it would be good to have it documented.
----
Regarding __Simon PJ__``'s earlier comment
{{{
It's easily stopped, too, by stopping GHC treating error like bottom;
but that would make many functions less strict. It'd be interesting to
measure the performance impact of this.
}}}
__Simon M replied:``__
It would be a shame if error wasn't treated as _|_, because that would
lose the opportunity to transform
{{{
Case error "foo" of alts ===> error "foo"
}}}
wouldn't it? This is only dead code elimination of course.
and __Simon PJ followed up with:``__
You are right that the strictness of an Id would have to distinguish:
* normal
* diverges (bottom)
* crashes (calls error)
Currently it does not. Changing the strictness analyser to make 'error'
look like 'normal' rather than 'diverges' would indeed have the effect of
making GHC not realise that (error "x") was a case scrutinee that could
be simplified.
So yes, there is a bit more to testing the effect of making 'error' less
strict than I was suggesting. Quite doable, but more than a moment's
work.
----
Regarding my strictness test
{{{
x = Bad xs => e = Bad ys and xs \subseteq ys
}}}
__Simon M__ suggested that an implementation might:
invent a magic exception X only used by the strictness analyser, and treat
this as
{{{
x = Bad X => e = Bad ys and X `elem` ys
}}}
All other exceptions (and _|_) can be mapped to the same thing; all that
matters is
whether x's exception was raised or not. I imagine you'd need to fiddle
around
with the strictness analyser's domain.
----
The sort of case where Simon PJ is worried we will lose performance is
{{{
f x [] = error "Can't happen"
f x (y:ys) = ... strict in x ...
}}}
where we would no longer be allowed to claim to be strict in x, as
{{{
f (error "X") []
}}}
should only throw "Can't happen". Debatably it's better to tell the
compiler explicitly that you want it to be strict in x with
{{{
f !x [] = error "Can't happen"
f !x (y:ys) = ... strict in x ...
}}}
anyway, rather than relying on the strictness analyser to figure it out.
----
Finally, I am not entirely convinced by the semantics of imprecise
exceptions as given in the paper; they tend allow too many exceptions to
be thrown, possibly under the assumption no compiler would actually
transform a program in such a way that
the unexpected exceptions actually would be thrown.
For example
{{{
(error "A") (error "B")
}}}
is permitted to throw B, even though
{{{
error "B"
}}}
would never be evaluated under non-strict evaluation.
Similarly,
{{{
case error "A" of
True -> error "B"
False -> 'x'
}}}
is allowed to throw B.
Incidentally, I do think it is reasonable for
{{{
case error "A" of
True -> error "B"
False -> error "B"
}}}
to throw B.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1171>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
