Re: [Haskell-cafe] phantom types
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
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
participants (2)
-
Florian Hartwig -
TP