Coinductive proofs of type class instances

[Louis Wasserman]

Hey all,

There was a discussion<http://www.nabble.com/Resolving-overloading-loops-for-circular-constraint-graph-td25365212.html>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 at gmail.com
http://profiles.google.com/wasserman.louis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20091028/37a74c15/attachment.html