[Haskell-cafe] help with MPTC for type proofs?

[David Roundy]

Hi all,

I've been thinking about extending some (experimental) GADT-based proof
code that verifies that the darcs patch theory code is properly used.  A
given patch has type (Patch a b), and I'd like to be able to write
something like

commute :: (Patch a b, Patch b c) -> (Patch a d, Patch d c)

in such a way that the type system know that the type d is one particular
type, uniquely determined by the types a, b and c.  Currently, which I do
is to make d be existential with

data Pair a c where
   (:.) :: Patch a d -> Patch d c -> Pair a c

commute :: Pair a c -> Pair a c

which prevents misuse of the returned pair, but doesn't allow proper use,
for example we ought to be able to compile:

test (a :. b) = do (b' :. a') <- return $ commute (a :. b)
                   (b'' :. a'') <- return $ commute (a :. b)
                   (a''' :.  b''') <- return $ commute (b' :. a'')
                   return ()

but this will fail, because the compiler doesn't know that b' and b'' have
the same type.

So I'd like to write something like

class Commutable a b d c

commute :: Commutable a b d c =>
           (Patch a b, Patch b c) -> (Patch a d, Patch d c)

But for this to work properly, I'd need to guarantee that

1. if (Commutable a b d c) then (Commutable a d b c)

2. for a given three types (a b c) there exists at most one type d
   such that (Commutable a b c d)

I have a feeling that these may be enforceable using fundeps (or associated
types?), but have pretty much no idea to approach this problem, or even if
it's soluble.  Keep in mind that all these types (a, b, c and d) will be
phantom types.

Any suggestions would be welcome.
-- 
David Roundy
http://www.darcs.net