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

[Ian MacLarty]

On Mon, Jun 05, 2006 at 04:07:44PM +1000, Mark Brown wrote:
> 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?
> 

Or just:

:- opaque type foo.

Since it's a dummy type there's no need to actually define foo (indeed
it wouldn't be opaque any more if you did :-)

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