[mercury-users] Exceptions, determinism and purity

[Julien Fischer]

On Fri, 7 Mar 2008, Nicholas Nethercote wrote:

> Hi,
>
> Take this predicate:
>
>  :- pred p(int::in) is det.
>
> It is det and doesn't produce any output.  So at first glance you'd think you 
> could safely remove any call to it.
>
> But, it could be defined like this:
>
>  pos(X) :- ( if X >= 0 then true else error("negative!") ).
>
> So removing calls could clearly change a program's behaviour.
>
> So it seems that exceptions/aborting falls outside of the determinism system. 
> Well, I realise that 'erroneous' is interpreted as "guaranteed to have a 
> solution;  has at most 0 solutions", but I'm struggling to see how that 
> theoretical viewpoint and the practical reality (eg. "can I remove this 
> call?") meet.
>
> Is the answer just "you can't remove any call to any predicate"?  Then it's 
> more like 'pos' has some kind of impurity.
>
> Does the Mercury manual address this?

Yes, see the ``Semantics'' section of the reference manual.  In
particular a goal like the above can only be optimised away if the
--no-fully-strict option is enabled (this allows the compiler to improve
completeness by optimising away non-terminating or errononous calls.)

The default is --fully-strict, which means that a goal can only be
optimised away** if (1) it is pure, (2) it is det (or cc_multi), (3)
it has no outpus, (4) the compiler can prove that it terminates and (5)
the compiler can prove it won't throw an exception, i.e. removing the goal won't
alter the operational behaviour of the program.  (The compiler's ability
to detect the latter two conditions varies depending on whether things
like termination analysis are enabled.)

** Obviously goals that compiler can prove will never be executed can
be safely optimised away as well, regardless of where they fall within
the above criteria.

Julien.
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------