[mercury-users] type-equivalence for DUs

[Ralph Becket]

doug.auclair at logicaltypes.com, Wednesday, 15 March 2006:
> I wish to define my own equality for a simple DU:
> 
> :- type espresso ---> single(float); duo(float, float)
>         where equality is coffee_goodness.
> 
> The compiler complains at my "ignore args" equality:
> 
> :- pred coffee_goodness(espresso::in, espresso:in) is semidet.
> coffee_goodness(single(_), single(_)).
> coffee_goodness(duo(_, _), duo(_, _)).
> 
> Saying that unification may fail.  I thought that's what
> 'semidet' meant.  Any rewrite of the above that I've
> tried leads to the same error, e.g.:
> 
> coffee_goodness(A, B) :-
>   A = single(_) -> B = single(_); B = duo(_, _).
> 
> The refman documentation isn't helping me any more ... what
> am I doing incorrectly?

Section 7 of the Reference Manual tells you what you should do
in precise, albeit unfriendly, language.

The most relevant parts are:

# If the program contains any deconstruction unification or switch on a
  variable of type T that could fail, other than unifications with mode
  (in, in), then it is a compile-time error.
# If the program contains any deconstruction unification or switch on
  a variable of type T that cannot fail, then that operation has
  determinism cc_multi.

This means you need to take a two-step approach:

coffee_goodness(A, B) :-
	promise_equivalent_solutions [Same] same_num_shots(A, B, Same),
	Same = yes.

:- pred same_num_shots(espresso::in, espresso::in, bool::out) is cc_multi.

same_num_shots(single(_), single(_), yes).
same_num_shots(single(_), duo(_, _), no).
same_num_shots(duo(_, _), single(_), no).
same_num_shots(duo(_, _), duo(_, _), yes).

The reason why you have to do this in two steps is that types with
user defined equality are non-canonical (i.e., the same value may
have many different, equivalent, representations), hence deconstructions
of such things must occur in committed-choice contexts.  And cc contexts
are not, generally, fun places to be for long.

We recognise that this is rather painful and Zoltan and Fergus are
working on a proposal that will make life easier.

-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------