Hello,<br><br><div class="gmail_quote">On Wed, Jun 15, 2011 at 10:49 AM,  <span dir="ltr">&lt;<a href="mailto:dm-list-haskell-prime@scs.stanford.edu">dm-list-haskell-prime@scs.stanford.edu</a>&gt;</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>
&gt;<br>
&gt; Hello,<br>
&gt;<br>
&gt; On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones &lt;<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>&gt;<br>
&gt; wrote:<br>
&gt;<br>
&gt;     | &gt;    class C a b | a -&gt; b where<br>
&gt;     | &gt;      foo :: a -&gt; b<br>
&gt;     | &gt;      foo = error &quot;Yo dawg.&quot;<br>
&gt;     | &gt;<br>
&gt;     | &gt;    instance C a b where<br>
&gt;<br>
</div><div class="im">&gt;     Wait.  What about<br>
&gt;            instance C [a] [b]<br>
&gt;<br>
</div><div class="im">&gt; No, those two are not different, the instance &quot;C [a] [b]&quot; should also be<br>
&gt; 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 -&gt; b<br>
</div><div class="im">        class D a b | a -&gt; b<br>
</div>        instance (D a b) =&gt; 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 &quot;b&quot; is in the FD closure of &quot;a&quot;.  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 &quot;incomplete&quot; (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>
&gt; The general rule defining an FD on a class like &quot;C&quot; is the following logical<br>
&gt; statement:<br>
&gt; &quot;forall a b1 b2.  (C a b1, C a b2) =&gt; (b1 = b2)&quot;<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 &quot;semantic&quot; property.  Here it is in English:</div><div><br></div><div>For any three ground types &quot;a&quot;, &quot;b1&quot;, and &quot;b2&quot;, if we can prove that both &quot;C a b1&quot; and &quot;C a b2&quot; hold, then &quot;b1&quot; and &quot;b2&quot; 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>