[Haskell-cafe] phantom types

[Florian Hartwig]

> Hi,
>
> I am currently reading documentation on Generalized Algebraic Data Types:
>
> http://en.wikibooks.org/wiki/Haskell/GADT
>
> I have a question concerning this page. Let us consider the following code
> proposed in the page:
>
> ----------------------------------
> -- Phantom type variable a (does not appear in any Expr: it is just a
> -- dummy variable).
> data Expr a = I Int
>             | B Bool
>             | Add (Expr a) (Expr a)
>             | Mul (Expr a) (Expr a)
>             | Eq (Expr a) (Expr a)
>             deriving (Show)
>
> -- Smart constructors
> add :: Expr Int -> Expr Int -> Expr Int
> add = Add
>
> i :: Int  -> Expr Int
> i = I
>
> b :: Bool -> Expr Bool
> b = B
>
> eval :: Expr a -> a
> eval (I n) = n
> ----------------------------------
>
> I obtain the following error:
>
> Phantom.hs:27:14:
>     Couldn't match type `a' with `Int'
>       `a' is a rigid type variable bound by
>           the type signature for eval :: Expr a -> a at Phantom.hs:27:1
>     In the expression: n
>     In an equation for `eval': eval (I n) = n
>
> The wiki page explains:
>
> """
> But alas, this does not work: how would the compiler know that encountering
> the constructor I means that a = Int?
> """
>
> I don't understand. When we write "eval (I n) = n", as I is a constructor
> which takes an Int as argument, we are able to deduce that the type of n is
> Int; so the type of eval should be in this case "Expr Int -> Int".
> What do I miss?

Since the example uses phantom types, the type of n is not actually
related to the type of (I n). It is perfectly possible to have, for
example, a value of type Expr String created by the I constructor:

*Main> let expr = I 5 :: Expr String
*Main> expr
I 5
*Main> :t expr
expr :: Expr String

So if we define eval the way it is defined in the example, the
compiler cannot infer that the type of (I n) is Expr Int, even though
it knows that n's type is Int.
We could prevent the creation of values with the wrong types by only
exporting the smart constructors, but that is no help for the type
system.

Declaring eval as Expr Int -> Int would make the code compile, but
since eval should presumably include patterns for other types, such as

eval (B b) = b

which would have to be of type Expr Bool -> Bool, we cannot do that.

I hope I did not misunderstand your question and this helps.
Cheers,
Florian