[m-dev.] Unique Modes and Transaction Logic

[Mark Brown]

On Mon, Jul 7, 2014 at 5:39 PM, Paul Bone <paul at bone.id.au> wrote:
> 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,

Note that Mercury's modes aren't part of the declarative semantics
(the pure predicate calculus). They are in addition to it, and have
the effect of constraining the order of execution, which is part of
the operational semantics. The constraints are specified in sections
4.2, 5.1 and 5.2 of the language ref.

>> which is what I mean by 'insufficient'.

I have to agree that there are interesting logic programs that aren't
well-moded in Mercury. So aside from constraining the order of
execution, modes also constrain the programmer to some extent. But the
payoff for all Mercury programs is a faster execution model.

>> 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>.

I'm not seeing why this code:

    philosopher(X), io.write_string(X, !IO) then io.nl(!IO)

is better than this:

    solutions(philosopher, List), foldl(print_line, List, !IO)

I personally find the latter easier to understand.

>> 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).
>

Also io.print_line  ;-)


>> -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.

To me that code doesn't seem any harder to understand than it needs to
be. What are you saying the problem with it is?


>> -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.

For the record, I think this is the most interesting application of
transaction logic, particularly for planning.

Cheers,
Mark.