[m-dev.] A hole in the type system (typeclasses and user defined equality)

[Mark Brown]

On 24-May-2006, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> I want to provide my own equality predicate for lp_expr(V) which
> calls the post_eq_constraint method for type V.  If I write
> 
> :- type lp_expr(V) ---> ... where equality is eq.
> 
> :- pred eq(lp_expr(V), lp_expr(V)) <= linear_solver_var(V).
> 
> eq(A, B) :- ...
> 
> then I rightly get a compilation error saying that the type class
> constraint on eq/2 is not met in the context of eq/2 as equality for
> lp_expr/1.
> 
> Unfortunately the language does not allow me to place type class
> constraints on type definitions...

This is true.

> 
> Help!

I think the best thing you can do here is to define this equality as a
normal predicate operating on types lp_expr(V) with the constraint on V,
and either leave builtin equality as the default or replace it with
something that throws an exception (so that people are less likely to
use it by mistake).

Another option is to define type lp_expr/0 and make the V type
existentially quantified.  But I wouldn't recommend this approach since
you will lose a lot of static checking.

> 
> -- Ralph
> 
> [I recall that Richard O'Keefe made a good case some years ago for
> allowing such things, but various technical reasons were stated
> suggesting it was a bad idea (alas I haven't been able to dig up
> that thread from the archives).]

Neither have I.  But one problem might be similar to the problem with
existential types whereby you need to use 'new' to distinguish construction
unifications from deconstruction unifications.  The explicit distinction is
required because the type checker needs to know whether it can assume any
constraints on the type variable (deconstruction) or whether it has to solve
the constraints (construction), but without the explicit distinction this
information is not available until mode analysis.

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