Hey all, There was a discussionhttp://www.nabble.com/Resolving-overloading-loops-for-circular-constraint-gr...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. First consider the problem that GHC doesn't allow type equality constraints in class definitions, so for example,
class (F a ~ b) => Foo a b
In particular, if I wanted F a to be *uniquely* associated with A, I might say that
class (F a ~ b) => Foo a b | b -> a where type F a
As a result, F would be a *bijective type family*, enforced by the type system. Interestingly, the GHC docs suggest something like this as an implementation for functional dependencies in general:
class Foo a b | a -> b is equivalent to class (F a ~ b) => Foo a b where type Foo a
except, of course, the latter isn't implemented in 6.10.4. All of this is idealized though: if GHC allowed equality constraints in superclass contexts, then this would be nice. Here was my workaround: a type class Foo is essentially a list of methods foo1 :: Foo a => ..... foo2 :: Foo a => ..... Of course, if there are superclass constraints on Foo a, those are implicitly included here. My thought was that
class (F a ~ b) => Foo a b where foo1 :: (constraints1) => ...
is essentially equivalent to
class Foo a b where foo1 :: (F a ~ b, contraints1) => ...
save that everywhere we encounter a (Foo a b) constraint, we replace it with (Foo a b, F a ~ b). 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). This approach actually, I think, works out some coinductive issues, if we apply this approach to issues besides type equality constraints. Louis Wasserman wasserman.louis@gmail.com http://profiles.google.com/wasserman.louis