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: 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:
{-# 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