[Haskell-cafe] phantom types

[TP]

First, thanks for your answer.

On Friday, August 17, 2012 15:31:32 you wrote:

> 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.

I think that my problem came from the fact that I have misunderstood type 
variables.

We have seen that the function eval:

eval :: Expr a -> a
eval (I n) = n

yields a compilation error:

"""
Phantom.hs:37:14:
Couldn't match type `a' with `Int'
`a' is a rigid type variable bound by
the type signature for eval :: Expr a -> a
"""

A somewhat similar error is found at 
http://stackoverflow.com/questions/4629883/rigid-type-variable-error

test :: Show s => s
test = "asdasd"

yields a compilation error:

"""
Could not deduce (s ~ [Char])
from the context (Show s)
bound by the type signature for test :: Show s => s
at Phantom.hs:40:1-15
`s' is a rigid type variable bound by
the type signature for test :: Show s => s
"""

Both errors contain the expression "rigid type variable". The explanation in 
the Stack Overflow page made me understand my error:

test :: Show s => s means "for any type s which is an instance of Show, test 
is a value of that type s".

Something like test :: Num a => a; test = 42 works because 42 can be a value 
of type Int or Integer or Float or anything else that is an instance of Num. 
However "asdasd" can't be an Int or anything else that is an instance of Show 
- it can only ever be a String. As a consequence it does not match the type 
Show s => s.

The compiler does not say: «s is of type String because the return type of 
test is a String».

Identically, in our case, «eval :: Expr a -> a» means «for any type a, eval 
takes a value of type «Expr a» as input, and outputs a value of type a». 
Analogously to the above case, the compiler does not say «a is of type Int, 
because n is of type Int». 

The problem here is that (I n) does not allow to know the type of a. It may be 
of type Expr String as you have shown:

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

So we may have anything for «a» in «Expr a» input type of eval. These 
multiplicity of values for «a» cannot match the output type of the equation 
«eval (I n) = n» which is an Int. Thus we get an error.

Am I correct?

Thanks,

TP