[Haskell-cafe] Re: Phantoms

[Jason Dagit]

On Sat, Aug 16, 2008 at 1:12 PM, Ben Franksen <ben.franksen at online.de> wrote:
>
> Jason Dagit wrote:
> > On Wed, Aug 6, 2008 at 11:09 AM, Andrew Coppin
> > <andrewcoppin at btinternet.com>wrote:
> >
> >> I just (re)discovered that I can do things like
> >>
> >>  data Foo x = Foo Int Int
> >>
> >> Now "Foo Int" and "Foo Double" are, as far as the type checker cares, two
> >> completely different types, even though in fact they are the same. This
> >> is actually Quite Useful, in the particular case I'm working on.
> >
> > Phantom types are indeed useful for many things, but a bit of cautionary
> > advice.  If you start to depend on the phantoms for type safety AND you
> > export your data constructors then you run a serious risk of being type
> > unsafe.  Bonus points if you can demonstrate an equivalent of
> > unsafeCoerce# this way.
>
> This would be very bad, but I doubt it is possible.
>
> > Example:
> > fooCast :: Foo Int -> Foo Double
> > fooCast (Foo x) = Foo x
> >
> > On noes!  We just cast that Foo Int to a Foo Double without changing it!
>
> What's the problem?

It's not so bad if you keep in mind that it's possible.  Sometimes
it's exactly what you want.

>
> > It works because the value on the RHS is consider freshly constructed and
> > other than sharing x it is unrelated to the one on the LHS.
>
> Right. You must call the data constructor Foo in order to exploit that it
> has the type
>
>  Foo :: Int -> Foo a
>
> I don't see how this is not type safe, and I was not able to produce an
> #unsafeCoerce with this technique. One would need some
>
>  unFoo a -> a
>
> but the  a  in  data Foo a  is phantom, i.e. there is no thing of type  a
>
> in a Foo.


Ah, it seems that the example I remembered cooking up requires GADTs,
lexically scoped type variables and one unsafeCoerce#, so I guess it
can be dismissed on the grounds that it uses unsafeCoerce# internally.
 I only need that because to make my thing work I need the following:

data EqCheck a b where
     IsEq :: EqCheck a a
     NotEq :: EqCheck a b

(=\/=) :: C a b -> C a c -> EqCheck b c

Without unsafeCoerce# I don't see how to implement (=\/=).  But, if
you had that you could do the following:

(=\/=) :: C a b -> C a c -> EqCheck b c
a =\/= b | unC a == unC b = unsafeCoerce# IsEq
         | otherwise = NotEq

data C x y = C String

unsafeC :: String -> C x y
unsafeC a = C a

unC :: C x y -> String
unC (C x) = x

myCoerce :: forall a b. a -> b
myCoerce x = fromJust $
  do let ab = unsafeC "" :: C a b
     let aa = unsafeC "" :: C a a
     IsEq <- return $ aa =\/= ab
     return x

Actually, it turns out that this also requires ghc 6.6.  I just tried
this out in both 6.6 and 6.8 and it turns out that in 6.8 the type
checker was upgraded, in particular the way type checking works for
GADTs was refined and the above program is rejected.

I'm glad to see that myCoerce is not possible without using an
unsafeCoerce# yourself.

Thanks,
Jason