On Fri, May 26, 2006 at 08:39:28PM -0700, oleg@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