[m-dev.] Unique Modes and Transaction Logic

[Paul Bone]

On Sat, Jun 28, 2014 at 03:53:29PM -0400, Marcus Troyka wrote:
> I was reading through the section in the ref manual on unique modes and
> I came to the conclusion that the proposed implementation isn’t really
> sufficient. Incorporating side-effect semantics in a logically sound way
> is by no means simple, but there are some basic ‘rules of thumb’ that
> can be inferred from the literature on transaction logic and used to
> reason about it.

In your first sentence you say that you believe that "the proposed
implementation isn't really sufficient."  Could you explain why?
It looks like you want to add side effects to Mercury in order to solve some
problem.  However I don't know what problem you want to solve, so it's hard
to appreciate your solution

Lets create some definitions, to make sure we understand each other:
Side-effect means an effect that cannot be seen when looking at the
declaration.  Effect is more general, it includes side effects but also
includes any declared effect.  Effects or side effects can include updating
memory destructively, or changing something about the environment (writing a
file, opening a network connection etc).

Mercury doesn't have side effects.  All effects are visible from the
declaration of a predicate or function.  Either the predicate or function is
declared as impure or semipure, or some of it's arguments represent the
'state' that's being manipulated like the IO state.  By looking at the
declaration you can see if there are any possible effects, and because there
cannot be an effect that is not declared in the declaration, therefore
there are no side-effects.

Side effects are (usually) undesirable.  Mercury was designed so that side
effects where not possible and thus programmers could more easily understand
their code.  This is very important for debugging, one can see at a glance
if a predicate either interacts with the outside world or destructively
updates memory.  If neither is true the programmer knows that certain errors
cannot be caused by that predicate.  Making side effects impossible also
allows compilers to more easily optimise code.  The compiler can re-order
conjuncts to improve locality of reference, or to avoid the creation of
intermediate data structures (deforestation).  The compiler can also choose
to execute some conjuncts in parallel using multiple cores.  This is
generally not possible when a language includes side effects.

Thanks.


-- 
Paul Bone