[mercury-users] hi & a feq queries

[Fergus Henderson]

On 18-Aug-1998, Thomas Charles CONWAY <conway at cs.mu.OZ.AU> wrote:
> Donald Syme, you write:
> > Thanks for your help.  Re. this last example: the point I was making
> > was that the compiler has different behaviour on beta-equivalent forms,
> > which surprised me, given Mercury is a pure language.

In general, it is quite possible for two programs to be logically
equivalent but for only one of them to be mode- and determinism-correct.
So the fact that two programs are logically equivalent doesn't mean that
the compiler will necessarily either accept both or reject both.

> > The "binding
> > of the non-local variable" (a rather operational way to look at it)

Yes, modes in Mercury are primarily an operational notion.
A specification only needs to be type-correct.  But for a program
to be executable, it also needs to be mode-correct.

(Lee Naish has done some work on a more declarative notion of modes,
which looks quite promising.  But it seems that the Mercury compiler 
needs an operational notion of modes in order to generate efficient
code.)

> > The "binding
> > of the non-local variable" (a rather operational way to look at it)
> > is clearly ok. in such limited cases.  But it's no big deal.
> 
> The binding of the non-local is a problem because at the time when
> the closure is constructed, the compiler doesn't know if it will be:
> 	called zero times
> 	called excatly once
> 	called more than once
> 
> If it is called zero times, then the predicate contains a mode error,
> because it does not satisfy its mode declaration (X would be free on
> success, not ground as declared).
> 
> If it is called excatly once, all is well.
> 
> If it is (or may be) called more than once, there are problems [...]

We have considered allowing some kind of "call-once" modes for higher
order predicates which would require them to be called exactly once, but
which would then allow them to bind non-local variables.  However,
figuring out all the details and specifying it exactly would be a fair
bit of work, and implementing it would be a lot of difficult work.
Furthermore, we didn't find any compelling examples where this sort of
feature would be needed.  So language simplicity and ease of implementation
considerations meant that this idea never really got off the ground.

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