[m-dev.] not_reached inst

[Ian MacLarty]

On Thu, Apr 12, 2007 at 12:12:56AM +1000, Simon Taylor wrote:
> On 11-Apr-2007, Ian MacLarty <maclarty at csse.unimelb.edu.au> wrote:
> > On Wed, Apr 11, 2007 at 02:43:31PM +1000, Simon Taylor wrote:
> > > On 11-Apr-2007, Ian MacLarty <maclarty at csse.unimelb.edu.au> wrote:
> > > > I've been reading David Overton's PHD thesis and discovered the not_reached
> > > > inst.
> > > > 
> > > > I would find it useful to use this inst in some Mercury code that is being
> > > > automatically generated.  The not_reached insts is however not documented
> > > > anywhere in the reference manual.  Could we make the not_reached inst
> > > > "official" by documenting it in the reference manual?  Are there any problems
> > > > with using the not_reached inst in Mercury programs?
> > > 
> > > In what context do you want to use not_reached insts?  What would the
> > > documented behaviour be?
> > 
> > What I want is the inst bound({}) (where {} is the empty set) which, according
> > to Overton's PhD, is what not_reached is defined as.
>  
> > Now it may be the case that class d is empty (perhaps because no members of d
> > have been added to the ontology yet).  In this case I'd like to be able to
> > generate the inst:
> > 
> > :- inst d == not_reached.
> > 
> > but still have the same modes as above, so that developers could write
> > and compile code using the d inst (even though no procedures that used
> > the d inst could ever be called).
> 
> OK, allowing `not_reached' or some way to write `bound(unique, [])' in user
> code is probably a reasonable way to deal with this, but it hasn't been well
> tested.  I'm not sure that the compiler will handle it correctly because of
> the assumption that not_reached insts only occur after a goal that cannot
> succeed.

Point taken.  I expected not_reached to behave differently than it currently
does.

> For example, inst_util.abstractly_unify_inst gives the unification
> of a not_reached inst with anything a determinism of `det', where it should
> probably be `failure'.
> 
> 	:- module inst_test.
> 	:- interface.
> 	:- type abc ---> a ; b ; c.
> 
> 	:- pred p(abc, abc, abc).
> 	:- mode p(in(not_reached), in, out) is nondet.
> 
> 	:- implementation.
> 	:- import_module std_util.
> 
> 	p(X, Y, Z) :- X = Y, Z = a.
> 
> inst_test.m:008: In `p'(in(not_reached), in, out):
> inst_test.m:008:   warning: determinism declaration could be tighter.
> inst_test.m:008:   Declared `nondet', inferred `det'.
> 
> A hack that might give you what you want without any change is to use a
> constructor in the bound inst that isn't valid for the type (e.g. bound([])
> for this example).  That should be illegal but currently the compiler doesn't
> check.
> 

I don't think that would solve the problem, since I'd still get a determinism
error (because the [] case wouldn't be handled).

The solution I have at the moment is to add an abstract types layer on top of
the insts. (For each insts there is an abstract type which is what is used in 
user code.  The types are converted to the correct insts as necessary.)

Ian.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------