[m-dev.] dummy types with user-defined equality/comparison

[Mark Brown]

On 05-Jun-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> On Tue, May 30, 2006 at 03:25:31PM +1000, Mark Brown wrote:
> > On 29-May-2006, maclarty at cs.mu.OZ.AU <maclarty at cs.mu.OZ.AU> wrote:
> > > On Mon, May 29, 2006 at 05:09:09PM +1000, Julien Fischer wrote:
> > > > 
> > > > Currently the compiler will abort when confronted with a dummy type that has
> > > > user-defined equality or comparison.  Below are two proposals for fixing
> > > > this.  Which do people prefer?
> > > > 
> > > > (1) Change the reference manual to say that discriminated union types
> > > >     whose body consists of a single zero-arity constructor may not have
> > > >     user-defined equality or comparison defined upon them.  (Plus change
> > > >     the compiler to emit the appropriate error mesages.)
> > > > 
> > > 
> > > I think this option is best, since if values of the type are restricted
> > > to one zero-arity function symbol then any two values of the type must
> > > compare as equal for all sound definitions of equality and comparison.
> > 
> > I agree that this option is best.
> > 
> > Note, however, that our intended interpretation of dummy types is not
> > meant to be reflected in the value given by the type declaration.  For
> > example, if the io.state type were defined as a dummy type then the
> > intent is that there are many different (i.e., not equal) values.  If
> > the compiler was allowed to reason that there is only one possible state
> > of the world, then it could in theory infer that main/2 means that same
> > as '='/2.  :-(
> > 
> > I don't think it's urgent that we do anything about this, though.  For the
> > way that dummy types like io and store are used, it is the unique inst which
> > gives the important information, not the type.
> 
> I think this is a very good point.  I also think the problem is more
> serious than Mark makes out.
> 
> As I understand it the common usage of dummy types would be to thread a
> pair of abstract values through predicates that update some state via
> side effects.  The dummy arguments allow us to make the predicate pure.
> The problem is that anyone looking at the code who applies declarative
> reasoning will rightfully come to the conclusion that the predicate can
> never update the dummy value, since they can see that it is a unit type.  
> We thus cannot reason declaratively about predicates with dummy
> arguments as they are currently defined.  What's worse is there is
> usually no impurity annotation on these predicates to alert us to the
> fact that we can't reason about them declaratively.
> 
> The fact that the compiler doesn't reason that predicates that only
> update their dummy arguments are the same as =/2 is not important.
> The issue is that a human reader may do so.

There is the final inst of `dead' which they should also consider.  But I
take your point.

> 
> I think the problem comes from the fact that dummy types are transparent
> when they should be opaque.

"Opaque" is a good word.  How about:

	:- opaque type foo ---> foo.

as a declaration?

(I would have also suggested s/opaque/abstract/, but we already use that
to mean something else.)

Cheers,
Mark.

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