impredicative type checking
Hello, I filed the following bug report: This produces a type error: foo :: forall b. (b -> String, Int) foo = (const "hi", 0) bar :: (forall b. b -> String, Int) bar = foo But the types are equivalent. The ticket was closed with a comment that the types are not equivalent. However, I don't see how they are not equivalent (in the presence of impredicative polymorphism) since I can write derivations for both forall b. (b -> String /\ Int) |- (forall b. b -> String) /\ Int and (forall b. b -> String) /\ Int |- forall b. (b -> String /\ Int) in intuitionistic logic. The counter example given on the bug tracker is: foo :: forall b. (b -> String, Int) foo = undefined x :: (String, String) x = case foo of (f, _) -> (f 'a', f True) which fails to type check where the other type signature would allow it to check. However, with impredicative polymorphism, this should type check. Perhaps it is too much to ask the inference engine to infer the type of f above. However, in the original code sample, there is no type inference necessary; it is just necessary to check if the two types unify, which they should given the standard interpretation of forall. Am I missing something here? -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.
Jeff Polakow wrote:
Hello,
I filed the following bug report:
This produces a type error:
foo :: forall b. (b -> String, Int) foo = (const "hi", 0)
bar :: (forall b. b -> String, Int) bar = foo
But the types are equivalent.
Once you cross the forall the type of b becomes fixed. case foo of (f,i) -> {- Here f is monomorphic :: b -> String -} case bar of (f,i) -> {- Here f is still polymorphic :: forall b. b -> String -} Think of how you would seal these with a newtype: newtype Foo = forall a. Foo (a -> String, Int) newtype F = forall a. F (a -> String) type Bar = (F,Int)
Jeff Polakow wrote:
However, I don't see how they are not equivalent (in the presence of impredicative polymorphism) since I can write derivations for both
forall b. (b -> String /\ Int) |- (forall b. b -> String) /\ Int
and
(forall b. b -> String) /\ Int |- forall b. (b -> String /\ Int)
in intuitionistic logic.
(Side-stepping your main point, rather, which I think Chris K answered correctly) This is a non-sequitur. The fact that A |- B and B |- A does not make them the same type. It makes them isomorphic types. I can prove (A \/ B) /\ C -| |- (A /\ C) \/ (B /\ C) but that doesn't mean "(Either a b,c)" and "Either (a,c) (b,c)" are the same haskell type. It does mean they are isomorphic types, neglecting bottoms. But isomorphic types are not the same type, for the type checker! Jules
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.
On 2008 Nov 12, at 10:53, Jeff Polakow wrote:
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.
Seems right to me: symbolically it may be an eta-expansion, but practically GHC's tuples are actually types, so the latter is a new tuple with a different type from the former. (GHC's handling of tuples is often infelicitous.) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
participants (4)
-
Brandon S. Allbery KF8NH -
Chris Kuklewicz -
Jeff Polakow -
Jules Bean