[mercury-users] Re: Determinism detection (Was Newbie problem.)

[Fergus Henderson]

On 16-Jun-1999, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> 
> There are a few issues here.
> 
> There is a basic conflict between abstraction and determinism
> detection: its nice to write code in an abstract way but compilers need
> more specific information in order to recognise determinism.
> 
> Determinism detection is so important for efficiency that LP languages
> typically sacrifice abstraction.  Inlining is the most obvious way to
> get both efficiency and abstraction.

Yes.  "For every problem, there is a solution which is simple, obvious --
and wrong."

> Typically it has been considered
> just an optimisation rather than an important language design feature.
> In Mercury, determinism detection is a very important part of the
> language, so there are grounds for considering inlining (or other
> mechanisms) more than just an optimisation.

Agreed.  But I would emphasise "other mechanisms".

> As a bit of an aside, NUE-Prolog allowed functions to be defined using
> == instead of =, to allow the programmer to specify the definitions
> should be inlined.  Thus in NUE-Prolog you can write efficient yet
> abstract code, for example:
> 
> nil == [].
> cons(H, T) == H.T.
> 
> append(nil, As, As).
> append(cons(A,As), ...

The trouble with this kind of language design is that it doesn't
support the critically important paradigm of design-by-contract.
The code may be abstract, but you have not documented what the abstraction
is, or what properties it must satisfy.  If I change the definition of
nil/0 and cons/2 (for example, I might want to change the representation
of lists so that I can do lazy concatenation), it's not clear what
properties I must preserve.  In NUE-Prolog, I could make a change
in one part of the program that exactly preserves the logical semantics
of that part of the program, and which preserves or improves the time/space
complexity of each individual operation, and yet it could still turn out
that this change causes a memory leak in some other part of the program.

Any approach based on inlining alone is going to suffer the same problem.
A seemingly innocuous change to the definition of a predicate in
one module may hide some information that turns out to be crucial
for determinism analysis of a predicate in a distant module,
cause a memory leak (in Prolog) or a compile error (in Mercury)
in the other module.

> Some have suggested declarations to say certain things are mutually
> exclusive.

Yes.  This supports a design-by-contract approach to programming,
avoiding the pitfalls described above.

> Note that in general these things will have multiple
> arguments, some output, so you need to be careful with quantifiers
> (the examples given are simplistic in this respect).

Yes.  Richard O'Keefe's and Peter Schachte's suggestions didn't
discuss situations with multiple arguments.

In general I'm pretty supportive of their general approach, but I would
like to see a more detailed and complete proposal.

> There are various issues to do with modules, and what determinism
> information should be attached to.  One possibility, which works pretty
> well in most cases I believe, is to attach it to types.

Attaching the information to types (e.g. by including the type name
in the declaration) sounds OK, but it would be a bad thing if the only
place that such information could be specified was type definitions,
because you might well define new sets of mutually exclusive predicates
operating on a given type long after you defined the type.
For example, for integers you could define predicates odd/1 and even/1,
and it would nice to be able to declare that they are mutually exclusive,
but there are many similar examples and they should not all need to be
built in to the definition of the `integer' type.

Cheers,
	Fergus.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------