On Fri, May 26, 2006 at 08:39:28PM -0700, [EMAIL PROTECTED] 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
