Hey all,<br><br>There was a <a href="http://www.nabble.com/Resolving-overloading-loops-for-circular-constraint-graph-td25365212.html">discussion</a> a while back about coinductive proofs of type class instances, discussing a problem I&#39;d encountered independently, and worked out a rough solution to.  I wanted to see if that solution had been reached by other people, and throw it into the mix.  My problem is slightly different, though, so it may not generalize.<br>

<br>First consider the problem that GHC doesn&#39;t allow type equality constraints in class definitions, so for example,<br><br>&gt; class (F a ~ b) =&gt; Foo a b<br><br>In particular, if I wanted F a to be <i>uniquely</i> associated with A, I might say that<br>

<br>&gt; class (F a ~ b) =&gt; Foo a b | b -&gt; a where<br>&gt;    type F a<br><br>As a result, F would be a <i>bijective type family</i>, enforced by the type system.  Interestingly, the GHC docs suggest something like this as an implementation for functional dependencies in general:<br>

<br>&gt; class Foo a b | a -&gt; b<br>is equivalent to<br>&gt; class (F a ~ b) =&gt; Foo a b where<br>&gt;   type Foo a<br><br>except, of course, the latter isn&#39;t implemented in 6.10.4.<br><br>All of this is idealized though: if GHC allowed equality constraints in superclass contexts, then this would be nice.<br>

<br>Here was my workaround: a type class Foo is essentially a list of methods<br><br>foo1 :: Foo a =&gt; .....<br>foo2 :: Foo a =&gt; .....<br><br>Of course, if there are superclass constraints on Foo a, those are implicitly included here.  My thought was that<br>

<br>&gt; class (F a ~ b) =&gt; Foo a b where<br>&gt;    foo1 :: (constraints1) =&gt; ...<br><br>is essentially equivalent to<br><br>&gt; class Foo a b where<br>&gt;    foo1 :: (F a ~ b, contraints1) =&gt; ...<br><br>save that everywhere we encounter a (Foo a b) constraint, we replace it with (Foo a b, F a ~ b). <br>

<br>Now, of course, we might have a (Foo a b) constraint in another superclass context, and have to recurse.  That might even be fine, though I haven&#39;t worked it out.  For this particular example, though, (Foo a (F a)) is equivalent to (F a ~ b, Foo a b).<br>

<br>This approach actually, I think, works out some coinductive issues, if we apply this approach to issues besides type equality constraints.<br><br clear="all">Louis Wasserman<br><a href="mailto:wasserman.louis@gmail.com" target="_blank">wasserman.louis@gmail.com</a><br>

<a href="http://profiles.google.com/wasserman.louis" target="_blank">http://profiles.google.com/wasserman.louis</a><br>