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

[David Roundy]

On Fri, May 26, 2006 at 08:39:28PM -0700, oleg at pobox.com wrote:
> 
> David Roundy wrote:
> > 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)
> 
> The problem seems easily solvable, exactly as described. We need to
> take care of the two requirements separately.

I guess what hasn't been addressed is the question I didn't know to ask...

I want the return type "d" to be a phantom type of some sort (although I'm
not clear on the distinction between phantom and existential types).
Ordinarily I'd do this with a GADT, which gives me a type that can't match
any other.  This at least is "safe", but what I want is to relax this
constraint.  So I'd like to return an existential type which contains the
constraint enforces this class.  (And I think I'm expressing this very
poorly!)

In short, I don't want to have to explicitely list which phantom types
commute, since the "a b" in Patch a b *will* be phantom, existential
types, so (as you say below) we can't list these instances explicitely:

> > instance Commutable' PL1 PL2 PL3 PL2I
> > -- If the latter is commented out, there will be an error in testab below
> > instance Commutable' PL1 PL2I PL3 PL2

> However, something tells me that the above approach isn't useful. We
> really would like to have as many patch labels as _dynamically_
> needed. Also, we probably would like to specify which patches commute
> dynamically, rather than statically. That is, we wish to examine the
> patches and only then conclude if they commute. Thus we need to
> program with evidence. The function commute becomes a semantic
> function: it really does something, at run-time. It examines the
> patches. If it decides the patches commute, it produces the pair of
> patches, marked with a unique and unforgeable type d -- along with the
> evidence that d is indeed determined by b, and vice versa. We need
> this evidence for the creative mixing of patches, as in the original
> test. This approach is not unlike the one described half a year ago,
> in response to a similar query:

Indeed, we definitely need to determine commutation dynamically, but I'd
like once that has been determined to be able to use the results statically
(see below).

>   http://www.haskell.org/pipermail/haskell-cafe/2005-December/012703.html
> 
> I still don't know if the were some problems with that
> approach. Anyway, here's the complete code:

I remember that email.  I ended up discarding the idea, when I realized
that the problem could be solved much more elegantly using GADTs as a type
witness (with unsafeCoerce#, admittedly), so that I don't need to
explicitely cast types.  I'm hoping that if we can come up with a static
solution to this (new) problem, I can again use GADTs to convert the static
solution to a dynamic one.

(Sorry if I'm being unclear... I suppose that's why I need to ask for help,
since I'm not sure what's possible or if possible how it'd be done...)
-- 
David Roundy
http://www.darcs.net