[mercury-users] functional dependencies question

[Mark Brown]

Hi Ian,

On 16-Jan-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
> Hello,
> 
> Why will a program with the following typeclass definitions not compile?
> 
> :- typeclass tc1(S, T) <= (S -> T) where [
> 	pred mem1(S::in, S::out) is det
> ].
> 
> :- typeclass tc2(S, T) <= tc1(S, T) where [
> 	pred mem2(S::in, S::out) is det
> ].
> 
> :- typeclass tc3(S) <= tc1(S, T) where [].
> 
> For tc2 shouldn't the compiler be able to infer that T is functionally 
> dependent on S, so mem2 is fine?

It would be able to infer that, but a deliberate design decision was
made to require the FDs on subclasses to be explicit.  The rationale
is that forcing them to be explicit would make code easier to
understand and reason about.

However, I don't consider this rationale to be particularly strong.  There
seems to be a bit of a "surprise" factor with this restriction, so I could
be persuaded that it would be okay to drop it.  (I was undecided about
this when I implemented it, so it seemed best to be conservative.)

> 
> For tc3 why does T need to be in tc3's arguments if it is functionally 
> dependent on S?

Functional dependencies allow us to relax the restrictions on predicate and
function contexts.  They don't allow the restrictions on other contexts to
be dropped.

> 
> The errors given by the compiler are:
> 
> fd.m:016: Error: type variable in superclass constraint is not a 
> parameter of this type class: tc1(_1, _3).
> 
> fd.m:022: Error: type variable in superclass constraint is not a 
> parameter of this type class: tc1(_1, _2).
> fd.m:019: In declaration for predicate `fd.mem2/2':
> fd.m:019:   error in type class constraints: type variable T occurs in 
> the
> fd.m:019:   constraints, but is not determined by the predicate's 
> argument
> fd.m:019:   types.
> 
> Is there a fundamental reason for these limitations or are they just 
> not yet implemented (or am I just being stupid ;-)

For the first limitation, neither; it was a deliberate decision.

For the second limitation, I believe it is fundamental.  The
"range-restrictedness" condition (that is, all variables on the RHS must
appear on the LHS) is necessary for completeness.  See [1] for details.

Cheers,
Mark.

[1] Duck, Peyton-Jones, Stuckey and Sulzmann, "Sound and Decidable Type
Inference for Functional Dependencies", ESOP 2004.

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