Hello,
Since you're already using GADTs, why not also use them to witness type
equality:
import GHC.Exts
data Patch a b = Patch Int Int
data Sequential a c where
Sequential :: Patch a b - Patch b c - Sequential a c
data MaybeEq :: * - * - * where
NotEq :: MaybeEq a b
IsEq :: MaybeEq a a
(=//=) :: Patch a b - Patch c d - MaybeEq b c
Patch _ x =//= Patch y _
| x == y= unsafeCoerce# IsEq
| otherwise = NotEq
sequenceIfPossible :: Patch a b - Patch c d - Maybe (Sequential a d)
sequenceIfPossible p q
| IsEq - p =//= q = Just $ Sequential p q
| otherwise= Nothing
Notice the usefulness of pattern guards. EqContext could be defined as
data EqContext :: * - * - * where
EqWitness :: EqContext a a
(though I ususally prefer to just call both the data type and the
constructor 'E'.)
Thomas
On Thu, 2005-12-08 at 09:23 -0500, David Roundy wrote:
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. Of course,
the huge advantage is that you can't use these functions to write buggy
code (at least in the sense of breaking the static enforcement of patch
ordering).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
