Hello!
On Thu, May 06, 1999 at 09:26:15PM -0400, Arvind wrote:
> [...]
> The optimization " n+1 > n ==> True " is extremely useful in array
> subscript analysis, bounds checking etc. and is correct as long as n
> terminates (is not bottom). The cases where this optimization is used
> most often, n usually terminates. A more diligent compiler would use
> the optimization only if it could prove that n does terminate. I will
> take my chances with a fast but less diligent optimizing compiler
> which in some diabolical cases produces 3 when it should not have
> terminated.
Why not define a rule
n+1 > n ==> n `seq` True
That IS semantically correct (for well-behaved instances of Num,
i.e. the rule should be restricted to the prelude instances of Num
which can't silently overflow --
n+1 > n == False where n == maxBound :: Int!).
Of course, there could be a rule
a `seq` b, where a /= _|_ ==> b
(where it's safe NOT to apply the rule if a /= _|_, but the
compiler can't prove it).
> Both the Id compiler and now the pH compiler follow this philosophy.
> May be we should let an implementation do whatever it pleases in case
> of an error. If we regard non-termination as an error then producing a
> value in case of non-termination may not seem so bizarre. However,
> there are many cases where I really do want my errors reported. I
> think such compiler/language decisions should be taken on pragmatic
> grounds.
Operationally, changing non-termination (or other forms of evaluation
to "bottom", such as really demanding the value of 1/0) into termination,
is a change of visible program behaviour. That is usually only viewed
as correct in an optimizer, if the change is merely speed...
> Arvind
Regards, Hannah.
