[m-dev.] Unique Modes and Transaction Logic
mark at mercurylang.org
Tue Jul 1 21:59:55 AEST 2014
On Sun, Jun 29, 2014 at 5:53 AM, Marcus Troyka <aeonioshaplo at gmail.com> 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.
> Firstly, ‘unique input’ is a tautology since all predicates can take ui
> as an input implicitly (which is how other predicates can be used in the
> goals of first order preds). I can't think of a situation where you
> would ever need to state ui explicitly.
The Reference Manual defines ui as `unique >> unique', meaning that
the input must still be unique at exit. It's needed to tell the caller
that you won't let the reference leak out via some other argument.
> The second thing, more important than io modes is the fact that pure
> predicate logic lacks semantics for describing order of evaluation or
> for formalizing the meaning and truth value of side-effects.
Mercury has both declarative and operational semantics, and it's the
latter that explains order of evaluation and side-effects such as
impure goals and trace goals.
> -Serial conjunctions like regular conjunctions are considered atomic,
> thus if a conjunction fails then all side-effects must be reversed. That
> being the case, predicates with io::di modes cannot be valid in
> ‘semidet’ or ‘nondet’ contexts, unless they provably occur after
> (serially follow) any term that can fail (thus avoiding the state
> changes altogether when failure occurs).
That may be reasonable for the io type, since the programmer always
needs to supply a final value at exit. But note that other types can
be simply discarded after being modified, and this rule for `di' would
not allow that.
More information about the developers