[m-dev.] Unique Modes and Transaction Logic

[Mark Brown]

Hi Marc,

On Fri, Jul 18, 2014 at 5:31 PM, Marcus Troyka <aeonioshaplo at gmail.com> wrote:
> Note, this isn't a reply to anyone in particular.
>
> I've been mulling this over for a while, and it seems that what I was
> thinking of doing wouldn't work well (or at all) simply because of the
> complexities of how predicates may be called.

Thanks for sharing your thoughts in any case.

I'm still just guessing what problem you are solving, though. The
first of the papers you referenced has two practical examples, one on
financial transactions and one on robot actions. The first example can
be expressed in Mercury using unique modes (section 5.1 of the
reference manual), and the second using "mostly unique" modes (section
5.2) and committed choice non-determinism (sections 6.4 and 6.5). So
Mercury's modes appear to be sufficient to address the problems raised
by this paper, at least.

> Even if a predicate is used as
> a fact, if it has an arity greater than 1 then determinism checking would be
> nontrivial and probably even impossible in many cases, whereas the actual
> implied meaning might not have been that complex.

Yes, perfect static determinism checking is not possible in general;
see the discussion in section 6.3. I dare say it is not possible to
prove much about `assert'.

(Transaction logic is not tied to `assert', though; you can choose a
different set of elementary operations. If instead of `assert' there
was an elementary operation like Mercury's map.set, that replaced any
existing row that had the same input values, then proving determinism
can be easy.)

> Handling limited mutable
> variables in a pure functional language would be much, much simpler (without
> multi and nondet), and is probably closer to what I actually wanted to do.
>
> On the other hand, given how much more complex everything is in logic, I
> don't see why anyone would want to use mercury for general purpose
> programming, or why catering to AI would not be included in mercury's goals.

I think Paul just meant that meta-interpretation like Prolog or Scheme
is not one of Mercury's goals, not that building
compilers/interpreters in general is not a goal.

> I mean, you could use OCaml (or similar) and get a similar level of purity
> without the confusing semantics and backtracking everywhere, which aren't
> useful very often in general programming anyway, and OCaml also includes OO
> semantics which are. Granted, learning logic has helped me to understand
> functional programming much better, but the more I learn the less I'm
> convinced that I would ever want that kind of flexibility unless it was
> absolutely necessary.

For my money, the biggest advantage of logic programming over
functional programming is that you can have multiple output arguments.
In functional syntax, if a procedure has more than one output you are
forced to either cram everything into the one return value, or else
make use of side effects.

Does OO necessarily entail side effects? The definitions of OO don't
seem to mention it, but every major OO system has them. Perhaps this
is only because they've chosen to use functional syntax for their
method calls, and don't want to use up the single output in returning
a final state?

>
> That said, I have a few other (random) ideas that are more important than
> transaction logic, but that'll have to wait for another thread.

Thanks again for sharing your thoughts.

Cheers,
Mark.

>
> Cheers
> -Marc T