[mercury-users] typeclass instance with functional dependency.

[Mark Brown]

Hi Max,

On 08-Sep-2009, Maxime Van Assche <mva at missioncriticalit.com> wrote:
> Hi,
>
> In the following test, the compiler complains about "Error: unbound type 
> variable Y in constraints on instance declaration.",
> while there is a functional dependency, which should (from my 
> understanding) bind that type.

This is the correct understanding for constraints on a predicate or
function signature.  Here the reason for requiring all type variables
to be bound is to ensure that the type of each call is unambiguous.

For constraints on instance declarations this is also a consideration,
but there is a more important one: the typechecker needs to be guaranteed
to terminate.  Essentially, we can't allow new variables to be introduced
while solving the constraints because this may lead us to try to solve
an infinite sequence of constraints instead of reporting a type error.

So the basic conditions for constraints on typeclasses and instances
(sections 10.6 and 10.7) are stricter than for constraints on predicates
and functions (section 10.5).  On instances, the functional dependencies
of the constraints help to satisfy the functional dependencies of the
typeclass itself, but they don't help with termination.

>
> Should this not throw an error?

With the existing conditions on instances, this is an error.

> And if so, can it be fixed easily?

Fixing it would require changing the language, but this is not
impossible.  The basic idea is that solving the typeclass constraints
must be guarateed to terminate somehow.  For example, rules along the
lines of requiring strictly fewer constructors and variables in each
constraint as in the head.  Once termination is guaranteed, only
relatively weak conditions are required to make the type system sound.

There is some discussion (from 2002) on the reviews list here:

<http://www.mercury.cs.mu.oz.au/mailing-lists/mercury-reviews/mercury-reviews.0204/0029.html>

For some discussion of another viable sets of rules, look for
"Paterson conditions" in this page:

<http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html>

Cheers,
Mark.

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