[Haskell-cafe] On GADT, phantom types, etc. terminology

[David Roundy]

On Mon, May 29, 2006 at 07:49:20PM -0700, oleg at pobox.com 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