[m-dev.] Type class instance constraints

[Ian MacLarty]

On Tue, May 22, 2007 at 04:27:44PM +1000, Mark Brown wrote:
> 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.
> 

What are the issues with lifting the restrictions for arguments that are in
the range of a functional dependency?  So for example we could write
instance declarations like:

:- instance stream.writer(gzip_writer(Stream), string, State)
	<= stream.writer(Stream, string, State).

Where stream.write(Stream, Unit, State) has functional dependency
Stream -> State.

Won't the functional dependency guarantee that there are no overlapping
instances?

Also won't the dictionary translation code work as is, since it must be
able to lookup the typeclass without knowing the State type?

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