[Haskell-cafe] phantom types

[Doaitse Swierstra]

On Aug 19, 2012, at 5:29 , wren ng thornton <wren at freegeek.org> wrote:

> 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

But if you use the real power of GADT's you would write:

{-# LANGUAGE KindSignatures, GADTs #-}
data Expr :: * -> * where
       I   :: Int                          -> Expr Int
       B   :: Bool                         -> Expr Bool
       Val :: a                            -> Expr a
       Add :: Expr Int -> Expr Int         -> Expr Int
       Mul :: Expr Int -> Expr Int         -> Expr Int
       Eq  :: Eq a => Expr a   -> Expr a   -> Expr Bool

eval :: Expr a -> a
eval (I i) = i
eval (B b) = b
eval (Val v) = v
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq e1 e2) = eval e1 == eval e2
> 


Note that the I and B cases are actually superfluous, and are covered by the val case. This has all nothing to do with phnatom types, but with a proper understanding of the GADT concept.

Doaitse

> 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
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe