[m-dev.] semantics with any insts

[Ian MacLarty]

On 4/3/06, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> On Mon, Apr 03, 2006 at 02:03:24AM +0200, Ian MacLarty wrote:
> > On 3/31/06, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> > > But in the absence of any insts, the old declarative names are
> > > appropriate;
> >
> > No they're not.  You have the same problem with partial instantiation,
> > or 'unused' modes.
>
> I thought Mercury didn't support partial instantiation?

Not fully at the moment (you can do some very simple partial
instantiation things), but it will be supported fully sometime in the
future.

> You're right
> about unused modes (I assume this is free>>free), but aren't they
> pretty much unused?  I can't see when you'd use one.
>

Ralph gave a good example.

> Anyway, the crux of my objection to turning determinism into (or
> accepting that it has become) an operational rather than a declarative
> thing, is that it then forces users, solver writers, and the Mercury
> implementation to commit to implementation decisions that should be
> changable.  Maybe today a solver writer implements a primitive
> constraint by backtracking over possible solutions because it's easy,
> and tomorrow does something clever to avoid backtracking.  It's just
> an implementation decision, but still all users of that constraint
> must now modify their code.
>
> 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.

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).  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.  It is
completely unrealistic to think that you are going to be able to
reason about only the declarative relationship between the arguments
of your predicates, ignoring how the computer should actually
calculate values, and still end up with an efficient program (except
for some toy examples).  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.

Ian.

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