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'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't allow type equality constraints in class definitions, so for example,<br><br>> class (F a ~ b) => 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>> class (F a ~ b) => Foo a b | b -> a where<br>> 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>> class Foo a b | a -> b<br>is equivalent to<br>> class (F a ~ b) => Foo a b where<br>> type Foo a<br><br>except, of course, the latter isn'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 => .....<br>foo2 :: Foo a => .....<br><br>Of course, if there are superclass constraints on Foo a, those are implicitly included here. My thought was that<br>
<br>> class (F a ~ b) => Foo a b where<br>> foo1 :: (constraints1) => ...<br><br>is essentially equivalent to<br><br>> class Foo a b where<br>> foo1 :: (F a ~ b, contraints1) => ...<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'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>