On Mon, May 29, 2006 at 07:49:20PM -0700, [EMAIL PROTECTED] wrote: > David Roundy wrote: > > I want the return type "d" to be a phantom type of some sort (although > > I'm not clear on the distinction between phantom and existential > > types). > > Well, they are, in a sense, dual to each other. [...]
Thanks for the explanation! :) > David Roundy wrote: > > when I realized that the problem could be solved much more > > elegantly using GADTs as a type witness (with unsafeCoerce#, > > admittedly) > > That is quite puzzling: the whole advantage of GADTs is that we don't > need to coerce values because type coercion, after checking the > run-time evidence (that is, successful pattern-match) is the very > essence of GADTs. The coersion is needed in order to generate the runtime evidence. If two patches (in identical context) are read from two repositories, we need to compare them at runtime in order to determine if their types are identical (which is the case if their contents are identical), so we have a function like data IsEq a b where Eq :: IsEq a a NotEq :: NotEq a b (=\/=) :: Patch a b -> Patch a c -> IsEq b c p1 =\/= p1 = if (check contents are equal) p1 p2 then unsafeCoerce# IsEq else NotEq which generates the runtime proof that the types b and c are actually identical. We need to coerce the type in order to add an additional constraint here. I don't think we can do this with only access to constructors, because that would make the code fail to typecheck. Which is the point, that with the above IsEq and phantom types, only with unsafeCoerce# (or if the two types have a common origin) can you generate evidence that two types are the same. > David Roundy wrote: > > Can someone explain to me why this doesn't work? > > > {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-} > > > module MPTC where > > > > > > class C a b c d | a b c -> d, a d c -> b > > > > > > instance (C a b c d) => C a d c b > > > > > > data P a b = P deriving (Show) > > > > > > data CommuteResult a b c where > > > CR :: C a b c d => (P a d, P d c) -> CommuteResult a b c > > When we abstract over |d|, there is generally no way to get the > original type back (short of various casts, which generally require > run-time evidence). One can think of it as upcast/downcast problem in > OO: we can always pretend that an object of the type A is an object of > a more general type ASuper (and any object is an object of the Top > type). However, downcasting from a value of a more general type to the > value of a more specific type requires some run-time evidence (even if > the more general value was obtained by the upcast from the desired > specific type). The nature of abstraction is to irreversibly forget -- > hence the encapsulation guarantee. If that is not desired, we can use > some other translucent, type-preserving, ways. For example, I generally understand, but would have thought that the class and its functional dependencies would stand as proof that the two d's are identical. I agree that we can't extract *what* the type d is, but given the above FD, we should be able to know that if (C a b c d) and (C a b c e) then d and e are the same type. What else is the use of functional dependencies? > > {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-} > > module MPTC where > > > > data P a b = P deriving (Show) > > > > data CommuteResult a b c = forall d. CR (P a (d b), P (d b) c) > > > > commute :: (P a (d b), P (d1 b) c) -> CommuteResult a b c > > commute (P, P) = CR (P, P) > > > > test (x,y) = do CR (y',x') <- return $ commute (x,y) > > CR (y'', x'') <- return $ commute (x,y) > > CR (x''',y''') <- return $ commute (y',x'') > > return () > > which type-checks... But with the above code, > test (x,y) = do CR (y',x') <- return $ commute (x,y) > CR (y'', x'') <- return $ commute (x,y) > CR (x''',y''') <- return $ commute (x'',y') > return () also typechecks, which is to say that we've missed the point of the exercise. > David Roundy wrote: > > I guess what hasn't been addressed is the question I didn't know to ask... > > It would help me personally to see the `ideal' code -- the code that > you wish to write and to typecheck. The code should be sufficiently > realistic (the IO can be stubbed though). I'll be out of town for a > week so unable to reply promptly. Okay. qHere's my dream code. I've commented out and marked with "currently fails" any tests that I can't already pass with my existing GADT-based (no classes involved) code. Actually, there are more properties that I'd like to implement, but this is a start, and just being able to do this would still be very nice. So the point is that all the "currently fails" code should typecheck when uncommented, and the "Must fail" code must cause the typecheck to fail. > module Main where > > import PatchCode ( P ( P ), commute, CommuteResult ( CR ) ) > > main = test (P, P, P) > > sametype :: a -> a -> IO () > sametype _ _ = return () > > test :: (P a b, P b c, P c d) -> IO () > test (x,y,z) = do -- sametype x y -- Will fail > _ <- return $ commute (y,z) > -- _ <- return $ commute (x, z) -- Must fail > CR (y',x') <- return $ commute (x,y) > _ <- return $ commute (x',z) > -- _ <- return $ commute (y', z) -- Must fail > CR (x_, y_) <- return $ commute (y',x') > _ <- return $ commute (y_,z) > -- _ <- return $ commute (x_, z) -- Must fail > -- sametype x_ x -- currently fails > -- sametype y_ y -- currently fails > CR (y'_, x'_) <- return $ commute (x,y) > -- sametype y'_ y' -- currently fails > -- sametype x'_ x' -- currently fails > -- _ <- return $ commute (y,x) -- Must fail > -- _ <- return $ commute (x',y') -- Must fail > -- CR (x__,y__) <- return $ commute (y',x'_) -- currently fails > -- sametype x__ x -- currently fails > -- sametype y__ y -- currently fails > return () Note that I haven't written any of the actual interesting code, just the "client" code that should be verified by the proof code. This is intentional, because I don't know how P and commute should be defined, or even CommuteResult. Actually, the type of "test" does depend on the kind of P, and you're welcome to change that type, keeping in mind that the type of test should reflect that we want a sequence of three patches. Just for completeness, let me provide my existing code, which passes the above as written, but fails the "currently fails" tests: > {-# OPTIONS_GHC -fglasgow-exts #-} > module PatchCode where > data P a b = P deriving Show > data CommuteResult a c where > CR :: (P a b, P b c) -> CommuteResult a c > commute :: (P a b, P b c) -> CommuteResult a c > commute (P, P) = CR (P, P) -- David Roundy _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe