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

[David Roundy]

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
>      <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 = ...

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