[Haskell-cafe] Re: [darcs-conflicts] how to nicely implement
phantom type coersion?
Ralf Hinze
ralf at informatik.uni-bonn.de
Thu Dec 8 10:00:26 EST 2005
> > 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))
More information about the Haskell-Cafe
mailing list