[m-dev.] Unique Modes and Transaction Logic

[Paul Bone]

On Tue, Jul 22, 2014 at 09:14:54AM -0400, Marcus Troyka wrote:
> On 07/21/2014 04:24 AM, Paul Bone wrote:
> > And that leads to the important distinction that an object breaks
> > referential transperancy but a module's pure procedures don't.
> I totally missed this before. That's not really true because an object
> is basically just a special type of closure. Also, now that I've looked
> it up I can say for certain that the OO system in OCaml actually works
> the way you suggested, using closures and threaded state to maintain
> purity.

I thought we'd covered this:
    + An object with internal state, breaks referrential transperancy.
    + An object with threaded state, does not break referrential
      transperancy.

Typically a class based OO system uses internal state, And I had previously
thought (possibly incorrectly) that a prototype based OO system typically
uses threaded state.


> However, I realized that external code/device calls cannot be completely
> pure (unless your program takes the entire universe as input!) nor
> treated as pure. Since functions/predicates like io.write_string() and
> io.read_line_as_string() produce a unique (as in different every time)
> output, at least from the perspective of your own (finite) code, they
> have to be di->uo. Device interfaces behave the same way. So you would
> end up with something more like:
> 
> > let ?? = Terminal.write_string("Hello, World!", !!) in/and..
> 
> and
> 
> > let p = Terminal.read_line_as_string(!!) in/and..
> 
> respectively.
> 

Now you've invented how the IO state is used in Mercury programs :-)

> On the other hand, any code that is /internal/ to your program should
> also be pure (esp with OO) so while I now understand how a pred can have
> types::modes like io::ui->string::uo, I still don't understand how any
> input could have mode 'ui' unless perhaps it were uo called in reverse,
> which isn't currently possible in mercury. Is there actually a real
> situation where "ui" can occur?

Remember that ui is unique >> unique.  Before the call the value is unique
(there are no other pointers to it), and after the call it is still unique.

Consider:

    :- pred lenght(list(X)::ui, int::out) is det.

    length([], 0).
    length([_ | Xs], Len + 1) :-
        length(Xs, Len).

After any call to length, either no extra pointers to the list are made, or
any pointers that are made to the list (or any part within it) are
no longer available (go out of scope).

When list is first executed: the pointer is checked, usually by checking
it's tag, to see which constructor applies, (the empty list, or the
non-empty list).  Checking this does not require duplicating the pointer and
in some cases (the C backends) does not require dereferencing the pointer.

If the list is the empty list.

    length([], 0).

This clause is entered, which does nothing more than return the value 0.  So
we now know that the base case preserves uniqueness.

If the list is the non-empty list.

    length([_ | Xs], Len + 1) :-
        length(Xs, Len).

Then the pointer to the list is dereferenced to retrieve the pointer to the
tail of the list (Xs).  So we've created a new pointer (Xs).  Then we make
the recursive call.  I'm doing a proof-by-induction so what I do now is
assume that the base case is the only possible thing that can happen because
it's the only thing I have uniqueness information about.  For the base case
we know from earlier that uniqueness is preserved, in this case it is
preserved that there is a single alias of Xs (the whole list) and we are
tracking that reference.  The final action of this clause is to add 1 to
Len, this doesn't affect uniqueness at all.

When this clause finishes, there are exactly two references to this list,
the whole list, and Xs.  And Xs goes out of scope when the clause finishes
so once we return to our caller we know that there is exactly one unique
reference to the list, so we've proven that uniqueness is preserved in both
clauses of this predicate.  We can use that information to re-evaluate the
recursive case (finishing the proof by induction), which concludes that for
_any_ call to length, uniqueness is preserved for it's first argument.

This currently doesn't work in Mercury because Mercury is unable to track
the set of pointers to some data.  But if it did work it would make
uniqueness easier to use and this would intern allow us to make programs
faster by using compile time garbage collection more aggressively.


-- 
Paul Bone