Hello,<br><br><div class="gmail_quote">On Wed, Jun 15, 2011 at 10:49 AM, <span dir="ltr"><<a href="mailto:dm-list-haskell-prime@scs.stanford.edu">dm-list-haskell-prime@scs.stanford.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
At Wed, 15 Jun 2011 10:10:14 -0700,<br>
<div class="im">Iavor Diatchki wrote:<br>
><br>
> Hello,<br>
><br>
> On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>><br>
> wrote:<br>
><br>
> | > class C a b | a -> b where<br>
> | > foo :: a -> b<br>
> | > foo = error "Yo dawg."<br>
> | ><br>
> | > instance C a b where<br>
><br>
</div><div class="im">> Wait. What about<br>
> instance C [a] [b]<br>
><br>
</div><div class="im">> No, those two are not different, the instance "C [a] [b]" should also be<br>
> rejected because it violates the functional dependency.<br>
<br>
</div>But now you are going to end up rejecting programs like this:<br>
<div class="im"><br>
{-# LANGUAGE MultiParamTypeClasses #-}<br>
{-# LANGUAGE FunctionalDependencies #-}<br>
{-# LANGUAGE UndecidableInstances #-}<br>
<br>
</div><div class="im"> class C a b | a -> b<br>
</div><div class="im"> class D a b | a -> b<br>
</div> instance (D a b) => C [a] [b]<br>
<br>
And a lot of useful code (including HList) depends on being able to do<br>
things like the above.</blockquote><div><br></div><div>Nope, this program will not be rejected because "b" is in the FD closure of "a". This stuff used to work a few GHC releases back, and I think that this is the algorithm used by Hugs.</div>
<div><br></div><div>A functional dependency on a class imposes a constraint on the valid class instances (in a similar fashion to adding super-class constraints to a class). In general, checking this invariant may be hard, so it is fine for implementations to be "incomplete" (i.e., reject some programs that do satisfy the invariant or, perhaps, fail to terminate in the process). OTOH, I think that if an implementation accepts a program that violates the invariant, then this is a bug in the implementation.</div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im"><br>
> The general rule defining an FD on a class like "C" is the following logical<br>
> statement:<br>
> "forall a b1 b2. (C a b1, C a b2) => (b1 = b2)"<br>
<br>
</div>And in fact b1 and b2 are equal, up to alpha-conversion. They are<br>
both just free type variables.</blockquote><div><br></div><div>No, this was intended to be a more "semantic" property. Here it is in English:</div><div><br></div><div>For any three ground types "a", "b1", and "b2", if we can prove that both "C a b1" and "C a b2" hold, then "b1" and "b2" must be the same type. The theory of functional dependencies comes from databases. In that context, a class corresponds to the schema for a database table (i.e., what columns there are, and with what types). An instance corresponds to a rule that adds row(s) to the table. With this in mind, the rule that I wrote above exactly corresponds to the notion of a functional dependency on a database table.</div>
<div><br></div><div>-Iavor</div><div><br></div><div><br></div></div>