On Sat, May 27, 2006 at 11:00:43AM -0400, Stefan Monnier wrote:
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
-- 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 = ...
It seems like the trouble with this sort of lemma is that it looks like you'd have to explicitly invoke it, which seems like an awful lot of work... I had been hoping that using class trickery, or some sort of type trickery, I could encode a set of properties that were automatically known by the type-checker. Sadly, the properties we're now talking about are the "easy" ones, and I had hoped that if they could be verified by the compiler, it would make it easier to prove the trickier patch properties! :( I'm beginning to suspect that what I want just isn't possible with Haskell in its current state. As Oleg points out, it could be done with FDs and classes, if we were willing to pass around explicit proof objects and run type coersion functions, but that seems awfully tedious--particularly when these "easy" properties are ones that we can do safely with no coersion required, and the motivation is to work towards making it easier to verify more difficult properties, which I fear would require a whole spaghetti of coersions. Ah well. I suppose can just slog along without these features until ghc 6.8 comes along with classes and GADTs living in harmony... I guess I've gotten spoiled by the nice checking I'm already able to do with just GADTs.
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.
I don't see how this gives us any safety. What guarantee would we have that a Commute a b c d actually corresponds to the result of a commute function? i.e. couldn't one use Comm_unique (undefined :: Commute Int Int Int x) (undefined :: Commute Int Int Int y) to prove that arbitrary types are identical? -- David Roundy http://www.darcs.net