how to nicely implement phantom type coersion?
Hello all, I've been working on a sort of static consistency-checking framework for darcs patches using GADTs and phantom existential types, and am looking for a bit of advice on whether I might be able to create a class to avoid some tedious coding overhead. 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. 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). So I'm wondering if there might be some sort of multi-parameter class one could define that would ease the use of an EqContext. For example I can imagine a (somewhat lame) class class EqTypes a b where safe_coerce_end :: Patch x a -> Patch x b safe_coerce_start :: Patch x a -> Patch x b safe_coerce_start = invert $ safe_coerce_end $ invert p (note that invert :: Patch a b -> Patch b a) then we could perhaps write some template haskell to define a couple of instances of EqTypes from a data type EqContext... except that I suspect that this is isn't possible, since the EqContext only exists at runtime, so unless one could define classes dynamically at runtime I'm out of luck. So is there some other approach that I can use for easily coercing phantom types based on runtime checks? Any suggestions? What I'd really love would be to be able to create a function that is polymorphic in kind rather than in type such as (inventing a rather poor syntax off the top of my head): data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) } where f(a,b) is a function of two types that returns a type, so the value of f(a,b) might be (Patch a b) or (Patch x b) or something like that. But I'm not sure if this is possible in Haskell, and if it is, then it definitely requires some sort of tricky extension that I'm not familiar with... -- David Roundy http://www.darcs.net
On Thu, Dec 08, 2005 at 09:23:22AM -0500, David Roundy wrote:
data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }
where f(a,b) is a function of two types that returns a type, so the value of f(a,b) might be (Patch a b) or (Patch x b) or something like that.
But I'm not sure if this is possible in Haskell, and if it is, then it definitely requires some sort of tricky extension that I'm not familiar with...
I'm a bit confused, but if you have: sc :: p a b -> p a c sc = unsafeCoerce# then (with Either standing in for Patch, PatchList etc and some concrete types as parameters to simplify things) sc (undefined :: Either Int Char) :: Either Int Bool is well-typed but sc (undefined :: Either Int Char) :: Either String Char isn't. Is that what you want? Thanks Ian
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))
Ralf Hinze wrote:
the type a :=: b defined below goes back to Leibniz's principle of substituting equals for equals:
If you like this, check out two of Ralf's papers: First-class phantom types: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR... Fun with phantom types: http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf The first (in section 2.4) explains a limitation of :=: I highly recommend both papers. Jim
On 12/8/05, David Roundy
So is there some other approach that I can use for easily coercing phantom types based on runtime checks? Any suggestions?
None here. Since H-M uses type unification to do type inference, you
can't auto-create a program based on the inferred types around it.
--
Taral
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).
On Thu, Dec 08, 2005 at 05:31:37PM -0500, Thomas Jger wrote:
Since you're already using GADTs, why not also use them to witness type equality:
Thanks for the suggestion! This just illustrates the rule that when using GADTs the solution to every problem is to introduce another GADT. It amazes me how many times that rule has proven true, and yet I *still* don't think to define a new GADT for every problem I run into... -- David Roundy http://www.darcs.net
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
participants (7)
-
David Roundy -
Ian Lynagh -
Jim Apple -
oleg＠pobox.com -
Ralf Hinze -
Taral -
Thomas Jäger