I'm reading Fun With Phantom Types. The first exercise asks why it is necessary to provide a signature to functions operating on Phantom Types. While I cannot come up with a general reason, I do see a problem in the following example:
data Expr a where
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
Eq :: (Eq a) => Expr a -> Expr a -> Expr Bool
whatIs (I _) = "an integer expression"
whatIs (Add _ _) = "an adition operation"
Now I understand that there are two possible types for whatIs
above, namely:
Expr a -> String
and
Expr Int -> String
however, the compiler instead gives an error:
• Couldn't match expected type ‘t’ with actual type ‘[Char]’
‘t’ is untouchable
inside the constraints: t1 ~ Int
bound by a pattern with constructor: I :: Int -> Expr Int,
in an equation for ‘whatIs’
at ti.hs:9:9-11
‘t’ is a rigid type variable bound by
the inferred type of whatIs :: Expr t1 -> t at ti.hs:9:1
Possible fix: add a type signature for ‘whatIs’
• In the expression: "someString"
In an equation for ‘whatIs’: whatIs (I _) = "someString"
• Relevant bindings include
whatIs :: Expr t1 -> t (bound at ti.hs:9:1)
I'm wondering why the compiler does not choose any of the two.
For your example,
Expr a -> String
is a strictly better type thanExpr Int -> String
: anywhere that anExpr Int -> String
could be used, anExpr a -> String
will certainly do. But sometimes there isn't a "weakest" or "strongest" type.Let's simplify your example even further:
Now here are two perfectly good types to give
eval
:These types aren't interchangeable! Each is useful in different situations. Compare:
So neither of these is more general than the other (and it turns out that no type is more general than both while still letting
eval
itself typecheck). Since there is no most-general type foreval
, it makes sense to refuse to pick a type and force the user to decide which of the many possible types they want this time around.