[m-dev.] Proposal: Sometimes it's safe to assume det=cc_multi

[Fergus Henderson]

On 07-Aug-2001, Holger Krug <hkrug at rationalizer.com> wrote:
> On Tue, Aug 07, 2001 at 02:54:24AM +1000, Fergus Henderson wrote:
> > On 06-Aug-2001, Holger Krug <hkrug at rationalizer.com> wrote:
> > > So why not to disallow `det' at all and rename `cc_multi' as `det',
> > ...
> > > Is code verification the only reason (admittedly a good one) ?
> > 
> > No.  There are several restrictions on `cc_multi' code,
> > which mean that there are important things that you can do
> > with `det' code which you can't do with `cc_multi' code:
> > 
> > (1) You're not allowed to backtrack into goals with determinism
> > `cc_multi'.  In other words, a goal with determinism `cc_multi'
> > cannot be followed in a conjunction by a goal with determinism `semidet'.
> > This restriction is needed to ensure soundness.
> > 
> > (2) Functions aren't allowed to have determinism `cc_multi'
> > in their standard mode (`func(in, in, ...) = out').
> > This restriction is needed to preserve referential transparency.
> 
> OK, I have to be more specific.
> 
> What if the compiler (determinism checker) derives something like:
> 
>   :- pred mypred(..., t , ...).
>   :- mode mypred(..., di, ...) is cc_multi.
> 
> in a place where the user has declared: 
> 
>   :- mode mypred(..., di, ...) is det.
> 
> Couldn't the compiler accept the user's declaration ? The unique mode
> `di' assures disallows backtracking. To maintain referential
> transparency it would additionally be required that the user cannot
> create values of type `t', e.g. that the type `t' somehow encapsulates
> `io__io'.  So the additional concept of a type, values of which cannot
> be created by the user would be necessary. 

Oh, right.   Yes, for procedures with io__state pairs,
the distinction between det and cc_multi is minor,
and could easily be abolished, without any problem for the semantics.
(This has been discussed previously on these mailing lists.)

If there is a concensus that the distinction between cc_multi and
det for procedures with io__state pairs is more trouble than it is
worth, then I'd be willing to get rid of it.

It wouldn't be necessary to change to the compiler.
We could just change the determinism of try_io
and any other cc_multi procedures in the standard library,
and we could provide a procedure

	:- pred io__choose(pred(T, io__state, io__state), T, io__state, io__state).
	:- mode io__choose(pred(out, di, uo) is cc_multi, out, di, uo) is det.

which let you call a cc_multi io procedure in a det io context.
(However, changing the compiler might be desirable, I'm not sure.)

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------