[Haskell-cafe] how to nicely implement phantom type coersion?

[Thomas Jäger]

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).