David Roundy wrote: ] The basic idea is that a patch will have type (Patch a b) where "a" and "b" ] are phantom types. Sequential patches will have identical ending and ] beginning types. So that a sequential pair, for example, can be written as ] ] data Sequential a c where ] Sequential :: Patch a b -> Patch b c -> Sequential a c ] ] The trickiness is that we need to be able to check for equality of two ] patches, and if they are truly equal, then we know that their ending states ] are also equal. We do this with a couple of operators: ] ] (=\/=) :: Patch a b -> Patch a c -> Maybe (EqContext b c) ] (=/\=) :: Patch a z -> Patch b z -> Maybe (EqContext a b) ] data EqContext a b = ] EqContext { coerce_start :: Patch a z -> Patch b z, ] coerce_end :: Patch z a -> Patch z b, ] backwards_coerce_start :: Patch b z -> Patch a z, ] backwards_coerce_end :: Patch z b -> Patch z a ] } ] ] where we use the EqContext to encapsulate unsafeCoerce so that it can only ] be used safely. The problem is that it's tedious figuring out whether to ] use coerce_start or coerce_end, or backwards_coerce_end, etc. I'd like to remark first that unsafeCoerce isn't actually necessary because the types to coerce to/from are phantom. If the data constructor is available, we can always `coerce' from one type to the other. The data type EqContext seems to be overkill. As I understand it, the problem is to be able to translate run-time equality of _values_ into an evidence that can later be used to interconvert values of two different _types_. As a side remark, such problems are often easier to solve if we write in CPS style (cf. for example, the Implicit Configurations paper). Anyway, the following code hopefully helps with the problem at hand:
{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}
module P where
In the real patch, the content of a patch is probably a string or an array of strings, or a file name. Integers should suffice here.
data Patch a b = Patch Int -- Hide the constructor (except for class Coerce) deriving Show
Suppose that our repository is in state S1 and we received a patch p1 (whose application takes the repository to state S2):
-- Patch p1 is applied to state 1 p1 :: Patch S1 S2 = Patch 1
We then received two patches p2 and p3 in parallel:
-- Patches p2 and p3 are both received in State 2 -- We don't know (yet) if they are the same though... p2 :: Patch S2 S3 = Patch 2 p3 :: Patch S2 S4 = Patch 2 -- the same patch actually
We can compose patches like this:
sequential :: Patch a b -> Patch b c -> Patch a c sequential (Patch x) (Patch y) = Patch (x+y)
s1 = sequential p1 p2 s2 = sequential p1 p3
*P> :t s1 s1 :: Patch S1 S3 *P> :t s2 s2 :: Patch S1 S4 The patches s1 and s2 are _intensionally_ the same but extensionally different. Indeed, if we try to place them in a list, we fail *> l1 = [s1,s2] Couldn't match `S3' against `S4' Expected type: Patch S1 S3 Inferred type: Patch S1 S4 In the list element: s2 In the definition of `l1': l1 = [s1, s2] There is hope however: creating a witness: EQP a b is a witness that the types a and b are the same. The value of the witness is not important...
data EQP a b = EQP -- Hide the constructor!
The following creates the proof:
(=\/=) :: Patch a b -> Patch a c -> Maybe (EQP b c) Patch x =\/= Patch y = if x == y then Just EQP else Nothing
(=/\=) :: Patch a z -> Patch b z -> Maybe (EQP a b) Patch x =/\= Patch y = if x == y then Just EQP else Nothing
We can now write
test1 = cons s1 s2 where cons s1 s2 | Just e <- p2 =\/= p3 = Just [s1, coerce s2 e] cons _ _ = Nothing
test2 = cons s1 s2 where cons s1 s2 | Just e <- p2 =\/= p3 = Just [coerce s1 e, s2] cons _ _ = Nothing
p4 :: Patch S2 S5 = Patch 4
test3 = cons s1 (sequential p1 p4) where cons s1 s2 | Just e <- p2 =\/= p4 = Just [coerce s1 e, s2] cons _ _ = Nothing
*P> test1 Just [Patch 3,Patch 3] *P> test2 Just [Patch 3,Patch 3] *P> test3 Nothing It should be stressed that we never had to worry if we have to coerce the start type of Patch or the end type of Patch, forward or backward. We just apply `coerce' (to whatever value) and the compiler figures out the rest -- what to coerce to what. The implementation
class Coerce a b c d e f | a b c d -> e f where coerce :: Patch a b -> EQP c d -> Patch e f coerce (Patch x) _ = Patch x
instance Coerce a b b c a c
instance Coerce a b c b a c
instance Coerce a b a c c b
instance Coerce a b c a c b
-- States of patching... data S1 data S2 data S3 data S4 data S5