[m-dev.] Type class instance constraints

[Mark Brown]

On 22-May-2007, Julien Fischer <juliensf at csse.unimelb.edu.au> wrote:
> 
> On Tue, 22 May 2007, Ralph Becket wrote:
> 
> >We currently have a number of restrictions on what can appear in an
> >instance declaration, namely that
> >
> >- each parameter takes the form type_name(TypeVar1, TypeVar2, ...)
> >- all TypeVars are distinct.
> >
> >These restrictions are there to prevent ambiguity with overlapping
> >instance declarations.
> 
> They are also there to ensure that typechecking terminates.

Exactly.  See [1] for a good explanation of the design space for typeclasses
in terms of CHRs.

> 
> >Given that is the case, why can't we lift both restrictions and simply 
> >check
> >for ambiguity at link time?  It would make the type class system much more
> >useful.  Currently the first restriction means you have to define no-tag
> >types all over the place and the second restriction prevents much useful
> >polymorphism.
> 
> Mark, is lifting these restrictions primarily a typechecking issue or
> an RTTI issue?  (I don't know that much about the former, but the latter,
> particulary for the second restriction, shouldn't be too much of a
> problem.)

It is:

(1)  A language issue.  Restrictions are necessary -- we need to choose a
set of restrictions such that the type system is sound and (semi) decidable.
It is one thing to suggest lifting individual restrictions, but the only
way to design this is to consider the typeclass system as a whole.

(2)  A typechecking issue.  The typechecker implementation assumes some of
the restrictions, and we will need to thoroughly comb through that code to
remove all those assumptions before we can expect it to work.  (NB: ever
since we came to understand the design space we have avoided making these
assumptions, but of course some of the code in the type checker is quite
old and predates that.)

(3)  A polymorphism issue.  The dictionary translation probably makes similar
assumptions to the tye checker.

(4)  An RTTI issue.  See Julien's comment on packing type_infos.  Reasoning
about our typeclasses implementation is difficult with this current
(premature, IMHO) optimization, so we plan to remove this optimization
first.

(5)  Another RTTI issue.  The name for the global variable generated for
the base_typeclass_info (the static data associated with an instance decl)
is derived from the arguments of the instance, and our name mangling
algorithm won't work without the current restrictions.  This might seem
trivial, but actually we currently implement the check for overlapping
instances in different modules by generating duplicate names, which is
detected at link time.  This only works because the current restrictions
mean that checking for overlapping instances is trivial -- there doesn't
seem to be any way to implement the full check using this technique, however.

(6)  A library metadata issue.  Since we won't be able to check for
overlapping instances using just the linker, we'll need to implement
it another way.  Without the current restrictions, the compiler or some
other Mercury-aware code will need to do the checking rather than the
linker.  It will need to get the information for this from somewhere,
and this information will of course need to be installed when installing
a library.  There is currently no kind of interface file that is suitable
for this task.


I think we need to address (1) before proceeding any further with discussions
about implementation.  We can also work on (4) and (6) in the meantime, since
those changes are useful in their own right.  (I believe Julien has been
working on (4) in his very limited free time.)

Cheers,
Mark.


[1] Sulzmann et al, "Understanding Functional Dependencies via Constraint
Handling Rules".  JFP (under consideration?)
<http://www.comp.nus.edu.sg/~sulzmann/publications/jfp-fds-revised.pdf>

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------