[m-dev.] semantics with any insts

[Peter Schachte]

On Mon, Apr 03, 2006 at 05:27:20AM +0200, Ian MacLarty wrote:
> > Assertions about the runtime behaviour of the code, rather than about
> > the meaning of the code, should be stated in some kind of pragma
> > declaration.
> 
> I dissagree. For me the appeal of Mercury is that I can impose both
> declarative and operation constraints on the programs I write and
> these two aspects are neatly separated:  The declarative constraints
> are in the type declarations and the operational constraints are in
> the mode declarations.

Prior to any insts, both of these were declarative.

> When I implement a predicate I must have both the declarative
> constraints in mind (the types) as well as the operational constraints
> (the initial and final insts of the arguments for each mode as well as
> the execution path(s) for each mode).

For correctness, you can ignore the operational constraints.  In
practice, many real problems are fairly small, and the simplest
implementation works well enough.  When it doesn't, *then* you can
worry about operational semantics.

> When the predicate compiles the
> compiler has verified that the declarative constraints are satisfied
> AND that the predicate will execute in the manner I expect.  I think
> you are playing down the importance of the latter point.

I'm not saying there shouldn't be operational declarations, I am just
emphasising the point that only correctness is really necessary, and
the necessary should be separated from the optional.

> Reasoning about your program both
> operationally and declaratively also leads to more reliable code,
> since you must think about your program in two different ways: 
> Reasoning declaratively about your program catches errors in your
> operational model and vica versa.

Very occasionally a performance bug indicates a correctness bug, but
not often in my experience.  And if there's a correctness bug, who
cares how efficient or inefficient the code is?

Gedanken experiment:  suppose Mercury supported a complexity
declaration for each mode.  Eg, append(in,in,out) is linear in the
length of the first argument, and qsort(in,out) is n*log(n) in the
length of argument 1.  It could be useful for the compiler to check
that the complexity of your code is what you think it should be.  But
do you think you should have to attach such a declaration to every
mode of every predicate you write?  Is it as important as getting the
types right?

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