Re: [Haskell-cafe] Re: Phantoms

On Sat, Aug 16, 2008 at 1:12 PM, Ben Franksen wrote:

Jason Dagit wrote:

...

On Wed, Aug 6, 2008 at 11:09 AM, Andrew Coppin 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