[m-dev.] Unique Modes and Transaction Logic

[Paul Bone]

On Mon, Jun 30, 2014 at 02:03:51PM -0400, Marcus Troyka wrote:
> On 06/29/2014 08:32 PM, Paul Bone wrote:
> > 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).
> This is really where our communication breaks down. When I say
> 'side-effect' what I mean is any output which cannot be directly passed
> as input to another function or predicate, whether or not the effect is
> explicitly declared. 'Side-effects' and 'effects' are basically the
> same, and the reason for that has more to do with the logical rules that
> govern them (or not). Assume, for example, that the following predicate
> represents all the 'facts' in the 'world' of our logical program:
> 
> :- pred philosopher(string::out) is det.
> philosopher("Socrates").
> 
> Now assume that in our 'main' predicate at some point we call:
> 
> assert(philosopher("Aristotle"), !IO)

Mercury doesn't have assert so this doesn't make sense.


> 
> our logical 'world' /after/ that becomes:
> 
> :- pred philosopher(string::out) is multi.
> philosopher("Socrates").
> philosopher("Aristotle").
> 
> Here we haven't really 'destroyed' the original value of
> philosopher("Socrates"), but now the predicate 'philosopher/1' has more
> than one solution whereas before it was det. The problem, and the reason
> that "side-effects" are "side-effects", is that pure predicate calculus
> has no concept of "unique outputs" or "before" and "after", and no model
> of what "the state of the world" means. The 'unique mode' semantics of
> Mercury isn't exactly wrong, but it isn't complete or formal either,
> which is what I mean by 'insufficient'.

Because you cannot change the meaning of philosopher in this way then you
don't need to understand if it is called "before" or "after" some other
code.

If you do want to correctly write something like the above example then the
best place to look is at Mercury's impurity annotations:
http://www.mercurylang.org/information/doc-release/mercury_ref/Impurity.html#Impurity

By default all code is pure, however you can declare predicates as semipure
or impure.  This gives us three choices, from top to bottom:

    + pure: This code does not affect other code,
            and cannot be affected by impure code.
    + semipure: This code does not affect other code,
            but may be affected by impure code.
    + impure: This code may affect impure and semipure code,
            and can be affected by other impure code.

So if you wanted to create a program that changed a set of facts for a
predicate philosopher/1 you'd declare it as:

:- semipure pred philosopher(string::out) is nondet.

And you'd also introduce:

:- impure pred assert_philosopher(string::in) is det.
:- impure pred retract_philosopher(string::in) is det.

Impurity controls the ordering of code that may be permitted.  Impure code
occurring to the left of either semipure or impure code is executed first.
Semipure code occurring to the left of other semipure code is executed first.
(If I remember correctly.)

This is sufficient to allow the programmer to use impure code (code with
side-effects) and semipure (code that may be affected by side-effects) where
necessary safely.  The compiler will check that this is used correctly and
emit compile-time errors if it is not.  Programmers are encouraged to write
pure code instead of using this, however there are times, such as when
interfacing with foreign code, when this is necessary.


> > 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.
> Transaction logic enhances all of those advantages while giving unique
> modes greater formality. Transaction logic models the 'state of the
> world' as a database which can have items inserted to or deleted from it
> atomically in a determined order. Changing the value of a 'mutable
> variable' in transaction logic means calling 'del:OldValue' serially
> followed by 'ins:NewValue' (that is, two transactions rather than one),
> and the distinction is important because while del->ins can be optimized
> to 'update in place' in some cases, it is not straightforward to infer
> 'del' and 'ins' from update-in-place semantics. Primitive atomicity of
> ins and del, combined with the reversibility of those operations allows
> 'assert' and 'retract' to be completely pure statements in transaction
> logic.
> 
> Abstractions aside, transaction logic would allow a number of
> significant improvements to mercury, including:
> 
> -The ability to use predicates with unique outputs in contexts with
> 'multi' deteminism. For example, something that is currently written
> like this <http://pastebin.com/P2Rv6Ju8> could instead be written like
> this <http://pastebin.com/0k3SmTrT>. Additionally, pure, reversible
> /assert/ and /retract/ semantics can even be used in semidet and nondet
> contexts without leading to inconsistent states.

There was a more general proposal to achieve something similar to this.  You
would still need to use solutions/2 to create a list but then you could
iterate over the list using a loop.

Also do you know that you can use list.foldl to help print out a list?

        foldl(print_item, List, !IO),

    :- pred print_item(string::in, io::di, io::uo) is det.

    print_item(String, !IO) :-
        write_string(String, !IO),
        nl(!IO).



> -The ability for the programmer to specify order of operations more
> precisely and flexibly, and for the compiler to more aggressively
> reorder and parallelize predicates that have unique modes.

I don't understand why the first point is necessary.  Why does the
programmer need to specify an order of operations when, provided that they
have used impurity where necessary their program will be correct and the
compiler is still free to optimise the unconstrained parts of it?


> -The ability to do things like construct an accumulator or design an
> object-oriented system in mercury using only pure, logical predicate
> semantics. In other words, using /assert/ and /retract/ instead of code
> that looks like this <http://pastebin.com/chceNbxs>, or foreign code.
> The predicate /mutate/ I mentioned is just syntactic sugar for
> "retract(Pred(X)) then assert(Pred(X1))".

Very few Mercury programmers actually need to write that kind of code
day-to-day.  It's probably not worth-while to implement transactional logic
just so we can re-write builtin_aggregate on it's own.

> -The ability for the compiler to provide more complete and consistent
> error checking for transactions (effects).

The effects that are supported by Mercury (IO) are checked, and the ones
that aren't are side-effects which are handled (and checked) safely by the
impurity declarations.  Without transactions we don't need error checking for
transactions.


> -There are also ways of using transaction logic in AI, and/or to reason
> about sequences of actions without committing them, although I admit
> that stuff is currently somewhat over my head.

Often the best way to experiment with AI is to write a new language and
interpreter/compiler.  Or use a language in which meta-interpretation is
already possible like Prolog or Scheme.  So I admit that you can't do this
directly in Mercury but I don't think that this is one of Mercury's goals.


> Anyway, I hope that answers your questions, or at least convinces you to
> read the original paper. :P

I admit, I'm curious, but for different reasons other than adding it to
Mercury.  Thanks for your e-mails and this information, I hope my and Mark's
feedback has been useful.


-- 
Paul Bone