[Haskell-cafe] phantom types

[wren ng thornton]

On 8/17/12 5:35 AM, TP wrote:
> 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)
> [...]
> 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?

Perhaps it'd help to rewrite the above ADT using GADT syntax (but note 
that its the exact same data type):

     data Expr :: * -> * where
         I   :: Int -> Expr a
         B   :: Bool -> Expr a
         Add :: Expr a -> Expr a -> Expr a
         Mul :: Expr a -> Expr a -> Expr a
         Eq  :: Expr a -> Expr a -> Expr a

So, when looking at the pattern (I n), since I :: Int -> Expr a we know 
that n :: Int and that (I n) :: Expr a.

-- 
Live well,
~wren