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

[Holger Krug]

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. 

Attempt of a definition:

1) values of an uc_type are called uc_values (uc = uncreatable)
2) `io__io' is an uc_type
3) T is a uc_type if it's an abstract type and all methods to create
   values of type T create one unique reference of type T in a 
   way which destroys another (uniquely referenced) uc_value 

Because T is an abstract type, the compiler should be able to decide,
if it's a uc_type based only on the module interface and the results
of checking for uc_types in other modules. 

For user convenience and transparency one would introduce syntax like:

:- uc_type io__io.

So we could say:

  cc_multi => det in the presence of unique modes and uc_types

This immediately would solve the issue we had with Ralph about
exception handling in imperative code (i.e. in the presence of unique
modes).

-- 
Holger Krug
hkrug at rationalizer.com
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------