The statements<br><br>class Cl [a] =&gt; Cl a<br><br>and<br><br>instance Cl a =&gt; Cl [a]<br><br>(I omit the type family constructor in the head for simplicyt)<br><br>state the same (logical) property:<br><br>For each Cl t there must exist Cl [t].<br>
<br>Their operational meaning is different under the dictionary-passing translation [1].<br>The instance declaration says we build dictionary Cl [a] given the<br>dictionary Cl [a]. The super class declaration says that the dictionary for Cl [a] <br>
must be derivable (extractable) from Cl a&#39;s dictionary. So, here <br>we run into a cycle (on the level of terms as well as type inference).<br><br>However, if we&#39;d adopt a type-passing translation [2] (similar to<br>
dynamic method lookup in oo languages) then there isn&#39;t<br>necessarily a cycle (for terms and type inference). Of course,<br>we still have to verify the &#39;cyclic&#39; property which smells like<br>we run into non-termination if we assume some inductive reason<br>
(but we might be fine applying co-induction).<br><br>-Martin<br><br>[1] Cordelia V. Hall,
<a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/h/Hammond:Kevin.html">Kevin Hammond</a>,
<a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/j/Jones:Simon_L=_Peyton.html">Simon L. Peyton Jones</a>,
<a href="http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wadler:Philip.html">Philip Wadler</a>:
Type Classes in Haskell.
<a href="http://www.informatik.uni-trier.de/%7Eley/db/journals/toplas/toplas18.html#HallHJW96">ACM Trans. Program. Lang. Syst. 18</a>(2): 109-138 (1996)<br><br>[2] Satish R. Thatte:
Semantics of Type Classes Revisited.
<a href="http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94">LISP and Functional Programming 1994</a>: 208-219<br><br><div class="gmail_quote">On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones <span dir="ltr">&lt;<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="im">| &gt; Hmm.  If you have<br>
| &gt;   class (Diff (D f)) =&gt; Diff f where<br>
| &gt;<br>
| &gt; then if I have<br>
| &gt;     f :: Diff f =&gt; ...<br>
| &gt;     f = e<br>
| &gt; then the constraints available for discharging constraints arising<br>
| &gt; from e are<br>
| &gt;     Diff f<br>
| &gt;     Diff (D f)<br>
| &gt;     Diff (D (D f))<br>
| &gt;     Diff (D (D (D f)))<br>
| &gt;     ...<br>
| &gt;<br>
| &gt; That&#39;s a lot of constraints.<br>
|<br>
| But isn&#39;t it a bit like having an instance<br>
|<br>
|    Diff f =&gt; Diff (D f)<br>
<br>
</div>A little bit.  And indeed, could you not provide such instances?  That is, every time you write an equation for D, such as<br>
<div class="im">        type D (K a) = K Void<br>
</div>make sure that Diff (K Void) also holds.<br>
<br>
The way you it, when you call f :: Diff f =&gt; &lt;blah&gt;, you are obliged to pass runtime evidence that (Diff f) holds.  And that runtime evidence includes as a sub-component runtime evidence that (Diff (D f)) holds.   If you like the, the evidence for Diff f looks like this:<br>

        data Diff f = MkDiff (Diff (D f)) (D f x -&gt; x -&gt; f x)<br>
So you are going to have to build an infinite data structure.  You can do that fine in Haskell, but type inference looks jolly hard.<br>
<br>
For example, suppose we are seeking evidence for<br>
        Diff (K ())<br>
We might get such evidence from either<br>
  a) using the instance decl<br>
         instance Diff (K a) where ...<br>
or<br>
  b) using the fact that (D I) ~ K (), we need Diff I, so<br>
        we could use the instance<br>
          instance Diff I<br>
<br>
Having two ways to get the evidence seems quite dodgy to me, even apart from the fact that I have no clue how to do type inference for it.<br>
<font color="#888888"><br>
Simon<br>
</font><div><div></div><div class="h5">_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>