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

[Ian MacLarty]

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.

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

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