On Wed, Aug 6, 2008 at 11:09 AM, Andrew Coppin
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. 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! 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. Note that by contrast this does not type check: foo :: Foo Int -> Foo Double foo f@(Foo x) = f Or, for that matter, any other variant where you don't use the constructor on the RHS. One way to get around this is to create your own constructor functions: mkFooInt :: Int -> Foo Int mkFooInt = Foo mkFooDouble :: Int -> Foo Double mkFooDouble = Foo Now export these instead of your data constructor. Similarly you'll probably want ones to take the place of pattern matching. The most obvious general purpose one being: unFoo :: Foo a -> Int unFoo (Foo a) = a But, if you're really relying on that phantom as a "witness", then you should probably define separate unFooInt :: Foo Int -> Int and unFooDouble : Foo Double -> Int. Here is the part where it gets really interesting. If you use GADTs, it rolls some of the above into one nice declaration: data Foo a where FooInt :: Int -> Foo Int FooDouble :: Int -> Foo Double I'm not sure if the GADT way can lead to an unsafeCoerce# equivalents or not. Maybe someone else can comment on that. Jason