[m-dev.] semantics with any insts

[Peter Schachte]

On Mon, Apr 03, 2006 at 01:31:13PM +1000, Mark Brown wrote:
> The usefulness of the operational reading is that the `nondet' _tells_
> the callers that the implementation is too inefficient!

Not necessarily.  It might mean the implementation is cleverly
handling the problem of data structures growing without bound by using
backtracking, so it only actually leaves a choicepoint when the only
alternative would be crashing or perhaps thrashing.

> The declarative
> reading will provide no help whatsoever in this case.

I'm not saying there should be no operational declarations, just that
we should be clear about which are declarative and which are
operational, and we should be reluctant to give up declarative
declarations.  I believe we should encourage declarative declarations
and discourage operational ones, except where they are critical to to
the user.

> If they don't like having to deal with this themselves they can use
> `--infer-all'

--infer-all doesn't work for exported predicates, and doesn't require
determinism declarations when they *are* declarative.  And has anyone
actually tested inferring any inst modes?

> Can you give an example of where the declarative reading would really
> benefit?

Sure.  The declarative reading of determinism helps me make sure I
handle all cases of a union type, and that IO is safe.  Both of these
currently go out the window with any insts.

If you mean the declarative reading of determinism for modes with some
final any insts, no I can't.  It's effectively always nondet, so
there's no declarative information to make use of.

> In fact, can you define what the declarative reading actually is?

Determinism specifies upper and lower bounds on the cardinality of the
success set.  That's how I've always thought of it, and I believe
that's how it was initially described to me.  Given that that is an
inherent property of the code, and that choicepoints and backtracking
are not the only possible way for Mercury to implement nondeterminism,
that's the only reading that will be stable over time.

> The
> existing definition in the reference manual talks about "inputs" and
> "outputs", but with the xor example both arguments are partly input and
> partly output.

"Output" just means the universal set of possibilities; "input" means
a singleton set of possibilities.  "Any" means any set of
possibilities, including the empty set.

-- 
Peter Schachte              The art of progress is to preserve order amid
schachte at cs.mu.OZ.AU        change, and to preserve change amid order.
www.cs.mu.oz.au/~schachte/      -- Alfred North Whitehead 
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
--------------------------------------------------------------------------