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

[oleg at pobox.com]

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