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. > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-undecidable-instances #-} > > module D1 where > > data Patch a b = Patch String deriving Show > > -- This is identical to what Tom Schrijvers wrote > class Commutable a b c d | > a b c -> d, -- 2. > a d c -> b -- based on 1. + 2. > > -- But how do we make sure that Commutable a d c b exists whenever > -- Commutable a b c d does? very easily: with the help of another > -- type class > instance (Commutable' a b c d, Commutable' a d c b) > => Commutable a b c d > > class Commutable' a b c d | a b c -> d > > -- The desired function > commute :: Commutable a b c d => > (Patch a b, Patch b c) -> (Patch a d, Patch d c) > commute ((Patch p1),(Patch p2)) = ((Patch p1),(Patch p2)) > > -- Testing > -- Define some patch labels > > data PL1 > data PL2 > data PL2I > data PL3 > data PL4 > > 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 > > pa :: Patch PL1 PL2 = Patch "PA: 1->2" > pe :: Patch PL2 PL3 = Patch "PE: 2->3" > > -- Test as was in David Roundy's message > test (a,b) = do (b',a') <- return $ commute (a,b) > (b'', a'') <- return $ commute (a,b) > (a''',b''') <- return $ commute (b',a'') > return () > > testab :: IO () = test (pa,pe) 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: I still don't know if the were some problems with that approach. Anyway, here's the complete code: > {-# OPTIONS -fglasgow-exts #-} > > module D2 where > > data Patch a b = Patch String deriving Show > > -- Define the commutation pair > data CP a b c = forall d. CP (Patch a d) (Patch d c) (EQP b d) > > data EQP b d = EQP -- Hide the constructor > > -- The following creates the proof > -- Assume patches commute if their bodies are the same > commute :: Patch a b -> Patch b c -> CP a b c > commute (Patch p1) (Patch p2) | p1 == p2 = CP (Patch p1) (Patch p2) EQP > > -- Testing > -- Define some patch labels > > data PL1 > data PL2 > data PL3 > data PL4 > > pa :: Patch PL1 PL2 = Patch "PA: 1->2" > pe :: Patch PL2 PL3 = Patch "PA: 1->2" > > -- coercion functions, using the evidence > a1 :: Patch a d -> EQP b d -> Patch a b > a1 (Patch p) EQP = Patch p > a2 :: Patch d c -> EQP b d -> Patch b c > a2 (Patch p) EQP = Patch p > > test a b = do CP b' a' e' <- return $ commute a b > CP b'' a'' e'' <- return $ commute a b > CP a''' b''' e''' <- return $ commute (a1 b' e') (a2 a'' e'') > return () > > testab :: IO () = test pa pe