[Haskell-cafe] Re: [darcs-conflicts] how to nicely implement phantom type coersion?

[Ralf Hinze]

> > data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }

I haven't seen the original post, so take the following with a
grain of salt. It seems that you are looking for a type that
models safe coercions. Here is one, the type a :=: b defined below
goes back to  Leibniz's principle of substituting equals for equals:
in every context `f' you can replace an `a' by a `b'.

Cheers, Ralf

---

Type equality.

> module TypeEq ((:=:), refl, symm, trans, (<>), list, pair, coerce, from, to)
> where

The type of type equality: |a :=: b| is non-empty iff |a = b|.

> newtype a :=: b               =  Proof { apply :: forall f . f a -> f b }

Equality is reflexive, symmetric, transitive and congruent.

> refl                          :: forall a . a :=: a
> refl                          =  Proof id
>
> newtype Flip f a b            =  Flip { unFlip :: f b a }
>
> symm                          :: forall a b . a :=: b -> b :=: a
> symm p                        =  unFlip (apply p (Flip refl))
>
> trans                         :: forall a b c . a :=: b -> b :=: c -> a :=: c
> trans p q                     =  Proof (apply q . apply p)
>
> (<>)                          =  trans
>
> newtype List f a              =  List { unList :: f [a] }
>
> list                          :: a :=: b -> [a] :=: [b]
> list p                        =  Proof (unList . apply p . List)
>
> newtype Pair1 f b a           =  Pair1 { unPair1 :: f (a, b)}
> newtype Pair2 f a b           =  Pair2 { unPair2 :: f (a, b)}
>
> pair                          :: a :=: c -> b :=: d -> (a, b) :=: (c, d)
> pair p1 p2                    =  Proof (unPair2 . apply p2 . Pair2 . unPair1 . apply p1 . Pair1)

Special casts.

> coerce                        =  apply
>
> newtype Id a                  =  Id { unId :: a }
>
> from                          :: forall a b . a :=: b -> (a -> b)
> from ep                       =  \ a -> unId (apply ep (Id a))
>
> newtype Inv a b               =  Inv { unInv :: b -> a }
>
> to                            :: forall a b . a :=: b -> (b -> a)
> to ep                         =  unInv (apply ep (Inv id))