inconsistent type checking behavior
Jeff Polakow
jeff.polakow at db.com
Wed Nov 12 10:53:01 EST 2008
Hello,
Thinking about this more, I have changed my mind about what should type
check, but I still think GHC's behavior is inconsistent...
> (Side-stepping your main point, rather, which I think Chris K answered
> correctly)
>
Chris explained that the types are not equivalent to GHC by showing a
context for which GHC's type checker differentiates the two types. My
point was that GHC is arguably wrong (but perhaps pragmatically correct).
The example Chris used assumes predicative polymorphism, but GHC
supposedly has impredicative polymorphism and under impredicative
polymorphism, I don't think there is a Haskell context which can
differentiate the two types. But this is a bit of a distraction from the
point I am trying to make which is...
GHC's type checker seems to have a bug or, at least, an infelicity. Here
is a description of the strange behavior which led me to this conclusion.
Note that all of the following is in GHC 6.10.1 with
-XImpredicativeTypes.
GHC's type checker accepts the following code:
b :: String -> forall b. b -> Int
b = \x y -> 0
f :: forall b. String -> b -> Int
f = \x y -> 0
GHC's also accepts the following code (I think this is wrong, see below):
b :: String -> forall b. b -> Int
b = \x y -> 0
f :: forall b. String -> b -> Int
f = b
Now, if we switch to an analogous, though slightly more complicated type,
GHC's type checker accepts the following code:
bar :: (forall b. b -> String, Int)
bar = (const "hi", 0)
foo :: forall b.(b -> String, Int)
foo = (const "hi", 0)
however GHC's type checker rejects the following code (I now think this is
correct):
bar :: (forall b. b -> String, Int)
bar = (const "hi", 0)
foo :: forall b.(b -> String, Int)
foo = bar
with the error :
Couldn't match expected type `b -> String'
against inferred type `forall b1. b1 -> String'
and yet GHC accepts the following code:
bar :: (forall b. b -> String, Int)
bar = (const "hi", 0)
foo :: forall b.(b -> String, Int)
foo = (fst bar, snd bar)
which is just the eta-expansion of the previous code.
This behavior seems inconsistent to me. I don't see any reason why the (f
= b) should be different than (foo = bar). In fact, thinking more
carefully about the types, I think that (f = b) should not type and the
eta expansion (f = \x -> b x) should be required.
> This is a non-sequitur.
>
On the contrary, this is the crux of the matter; derivations are type
checking. To figure out what should type check we need to look at what is
derivable.
> The fact that A |- B and B |- A does not make them the same type. It
> makes them isomorphic types.
>
True, the derivations are isomorphic, and in a language with explicit
type-lambdas and type-applications, there would be two different but
isomorphic terms for the two types. However, since Haskell leaves
type-lambdas and type-applications implicit, the exact same Haskell term
can have both types (as shown above). So it is not so crazy to think that
(f = b) and (foo = bar) might type check.
Furthermore, it is by looking at the typing derivation system that I've
come the conclusion that (f = b) should not type check. In order to type
check (f = b) we have to derive the following (assuming no explicit terms
for type-lambdas and type-applications):
b :: String -> forall a. a -> Int |- b :: forall b . String -> b ->
Int
which can't be done, whereas
b :: String -> forall a. a -> Int |- \x -> b x :: forall b . String
-> b -> Int
can be derived.
-Jeff
---
This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081112/e5015f85/attachment.htm
More information about the Glasgow-haskell-users
mailing list