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

[Stefan Monnier]

> I'm thinking that either the functional dependency constraint is weaker
> than I thought, or that somehow GADTs aren't interacting with FDs as I'd
> like, but I'm not sure which.  Or, of course, it may be that my recursive
> instance is not doing what I like.  Or I may be just plain confused, as is
> pretty clearly the case...

The interaction between FD and GADTs is not very good, in our experience.
Hopefully this will be fixed at some point.  But in the mean time, what we
ended up doing is to use GADTs instead of classes and FDs:

   data Eq a b where refl_eq :: Eq a a

   data Commute a b c d where
     <various axioms defining how D can result form A, B, and C>

   -- Lemma that says that D is uniquely defined by A, B, and C.
   Comm_unique :: Commute a b c d -> Commute a b c d' -> Eq d d'
   -- Proof.
   Comm_unique p1 p2 = ...

The problem is that in your case it seems that you do not want to explain to
the type checker how D depends on A B C: you just want to say that it's
uniquely defined.  But maybe you can get away with:

   data Eq a b where refl_eq :: Eq a a
   data Commute a b c d     -- No axioms provided to Haskell.
   -- Lemma that says that D is uniquely defined by A, B, and C.
   Comm_unique :: Commute a b c d -> Commute a b c d' -> Eq d d'
   -- The proof is not given either.
   Comm_unique p1 p2 = undefined

When you'll do a case on "Comm_unique a b" (which will tell the type checker
that D and D' are one and the same) you'll just want to make sure that
Haskell doesn't try to look at the `refl_eq' value.


        Stefan