[Haskell-cafe] Newbie question (again!) about phantom types

[Tillmann Rendel]

peterv wrote:
> I’m having difficulty to understand what phantom types are good for. 
> 
> I read the wiki, and it says "this is useful if you want to increase the
> type-safety of your code", but the code below does not give a compiler error
> for the function test1, I get a runtime error, just like test2.

> -- With phantom types
> data T1 a = TI1 Int | TS1 String deriving Show
> 
> foo1 :: T1 String -> T1 String -> T1 String
> foo1 (TS1 x) (TS1 y) = TS1 (x++y)
> 
> test1 = foo1 (TI1 1) (TI1 2) -- Shouldn't this give a compiler error instead
>                              -- of a runtime error? 

You have to manually instantiate the phantom type variable. In your 
code, the type of TI1 1 is just T1 a for an unrestricted type variable 
a. This unifies fine with the expected argument type of foo1, wich is T1 
String, by setting a = String. Consider this variant of your code:

   -- the type of things wich can hold numbers or text
   -- what exactly they hold is encoded dynamically by the
   -- constructor used and statically by the phantom type
   data Container a = NumberContainer Int | TextContainer String

   data Number = Number
   data Text = Text

   -- approbiate smart constructors. only use these for creation
   -- of containers, never use the real constructors.
   number :: Int -> Container Number
   number x = NumberContainer x

   text :: String -> Container Text
   text x = TextContainer x

   -- a function wich works only on containers holding text
   foo :: Container Text -> Container Text -> Container Text
   foo (TextContainer a) (TextContainer b) = text (a ++ b)

   -- testing
   test1 = text "hello " `foo` text "world" -- works
   test2 = number 13 `foo` number 19        -- static error

This works fine when you can decide statically how to instantiate the 
phantom type variable (by using the approbiate smart constructor). If 
you can't (because you read data from same external source, for 
example), you can restrict the position of dynamic failures to a 
well-defined point in program execution by defining

   asText :: Container a -> Maybe (Container Text)
   asText (TextContainer x) = Just $ text x
   asText _ = Nothing

   asNumber :: Container a -> Maybe (Container Number)
   asNumber (NumberContainer x) = Just $ number x
   asNumber _ = Nothing

Using these functions, you can lift a dynamic typecheck (is it the right 
constructor?) to a static typecheck (has it the right phantom type?). So 
you can for example check user input once for having the correct form 
and then enter the statically typesafe part of your program, where you 
don't have to worry about people entering numbers instead of text, 
because you statically know that at this point in program execution, the 
dynamic typecheck already suceeded.

   Tillmann