[m-dev.] Resources example

[Peter Schachte]

> The key thing about solver types is the `any' inst, which effectively
> says that the denotation of a variable with inst `any' can only be
> decided with respect to the current (implicit) constraint store state
> for that variable's solver type.

I think the interesting thing about the 'any' inst is that it makes no
commitment as to the number of distinct possible ground terms that a
particular term may represent.  But it probably is true that it would
be sufficient to have resources and the ability to specify
initialization and equality predicates in a type declaration to
provide solvers.  I don't think you really need separate solver and
representation types, just opaque types.

> Now, let's say `t' is a type implementing Herbrand terms, `cstore' is
> the resource carrying around the constraint store for `t' values, and Xs
> is a `list(t)'.  Now I want to call `contains_duplicate(Xs)' where
> 
> :- pred contains_duplicate(list(T)::in) is semidet.
> 
> contains_duplicate([X | Xs]) :- member(X, Xs).
> contains_duplicate([_ | Xs]) :- contains_duplicate(Xs).
> 
> In this case my call to `contains_duplicate' silently updates the
> `cstore' resource because unification for type `t' will update `cstore'.

True, just as a goal X = [] silently updates the heap.  The
interesting thing about your example with constraints is not that it
updates the constraint store, but that it works on non-free but
non-ground terms.

> Under these circumstances the compiler can't do things like optimize
> away duplicate calls to `contains_duplicate' *anywhere* that it can't
> prove that the unification predicate for whatever T doesn't use some
> resource.

Nope, because you've promised that unification (and all other
constraint predicates) only modify the constraint store in a
commutative and idempotent way.  If you haven't made that promise,
then you have to precede your calls to those predicates with ! to
specify that they may use and/or modify a resource in a possibly
non-commutative, non-idempotent way.  Goals with the ! at the front
cannot have those optimizations made, any more than goals that use
state variables or goals in DCGs can.

So no, resources don't affect the optimizations the compiler can do in
general.

-- 
Peter Schachte              The government of the United States is not, in any
schachte at cs.mu.OZ.AU        sense, founded on the Christian religion.
www.cs.mu.oz.au/~schachte/      -- George Washington, 1796 
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------