Hey all,
There was a discussion 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