RE: [Haskell-cafe] Functional dependencies and type inference
Einar Good question. This is a more subtle form of the same problem as I described in my last message. In fact, it's what Martin Sulzmann calls "the critical example". Here is a boiled down version, much simpler to understand. module Proxy where class Dep a b | a -> b instance Dep Char Bool foo :: forall a. a -> (forall b. Dep a b => a -> b) -> Int foo x f = error "urk" bar :: (Char -> Bool) -> Int bar g = foo 'c' g You would think this should be legal, since bar is just an instantation of foo, with a=Char and b=Bool. But GHC rejects it. Why? GHC looks at the call to foo (in bar's RHS), and instantiates it with a=Char. That tells it that the second argument should have type (forall b. Dep Char b => Char -> b) But it doesn't! It has type (Char -> Bool). And to GHC these are not the same types. You may say that they *should* be the same types. The crispest way I know to explain why it arguably should be rejected is to try translating the program into System F (which is what GHC actually does). Then the RHS of bar looks like bar (g::Char->Bool) = foo {Char} 'c' (...???...) The {Char} is the type argument to foo. But what can we pass for (...???...)?. We must pass a polymorphic function, with type forall b. Dep Char b -> Char -> b But all we have is g::Char->Bool. And System F has no way to connect the two. Well, that's the problem anyway. I can think of three "solutions": - Reject such programs (GHC's current solution) - Abandon compilation via System F - Extend System F I'm working on the third of these, with Martin, Manuel, and Stephanie. Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of | Einar Karttunen | Sent: 15 July 2005 13:48 | To: haskell-cafe@haskell.org | Subject: [Haskell-cafe] Functional dependencies and type inference | | Hello | | I am having problems with GHC infering functional dependencies related | types in a too conservative fashion. | | > class Imp2 a b | a -> b | > instance Imp2 (Foo a) (Wrap a) | > | > | > newtype Wrap a = Wrap { unWrap :: a } | > data Foo a = Foo | > data Proxy (cxt :: * -> *) | > | > foo :: Imp2 (ctx c) d => Proxy ctx -> (forall a b. (Imp2 (ctx a) b) => a -> b) -> c -> d | > foo p f x = f x | | The type of "foo (undefined :: Proxy Foo)" is inferred as | "forall c. (forall a b. (Imp2 (Foo a) b) => a -> b) -> c -> Wrap c" | which shows the outmost functional dependence is working fine. ctx | is carried to the inner Imp2. | | However "foo (undefined :: Proxy Foo) Wrap" will fail complaining that | | Couldn't match the rigid variable `b' against `Wrap a' | `b' is bound by the polymorphic type `forall a b. (Imp2 (ctx a) b) => a -> b' | at <interactive>:1:0-32 | Expected type: a -> b | Inferred type: a -> Wrap a | In the second argument of `foo', namely `Wrap' | | My guess is that GHC cannot see that the functional dependency | guarantees that there are no instances which make the inferred | type invalid. Any solutions to this problem? | | | - Einar Karttunen
Hello,
On 8/11/05, Simon Peyton-Jones
... Here is a boiled down version, much simpler to understand.
module Proxy where
class Dep a b | a -> b instance Dep Char Bool
foo :: forall a. a -> (forall b. Dep a b => a -> b) -> Int foo x f = error "urk"
Should this really be valid? It seems that because 'b' is determined by 'a' we should not be allowed to quantify over 'b' without quantifying over 'a'. I think we can view the class 'Dep' as a function on types, that is defined by the instances. Then the above type is: a -> (a -> Dep a) -> Int and it seems that the quantification over 'b' is non-sensical. -Iavor
Simon,
I believe there may be some nasty interactions with generalized
newtype-deriving, since we can construct two Leibniz-equal types which
are mapped to different types using fundeps:
class Foo a where
foo :: forall f. f Int -> f a
instance Foo Int where
foo = id
newtype Bar = Bar Int deriving Foo
-- 'Equality' of Int and Bar
eq :: forall f. f Int -> f Bar
eq = foo
class Dep a b | a -> b
instance Dep Int Bool
instance Dep Bar Char
newtype Baz a = Baz { runBaz :: forall r. Dep a r => a -> r }
conv :: (forall f. f a -> f b) ->
(forall r. Dep a r => a -> r) -> (forall r. Dep b r => b -> r)
conv f g = runBaz $ f (Baz g)
bar = conv eq
Here, after type erasure, 'bar' is the identity function . Ghc infers
bar :: (forall r. (Dep Int r) => Int -> r) -> Bar -> Char
This is not valid as an explicit type signature, but presumably the
proposal implies that we could type bar as
bar :: (Int -> Bool) -> Bar -> Char
instead. Now
\x -> bar' (const x) (Bar 0) :: Bool -> Char
would become an unsafe coercion function from Bool to Char.
Thomas
On 8/11/05, Simon Peyton-Jones
Einar
Good question. This is a more subtle form of the same problem as I described in my last message. In fact, it's what Martin Sulzmann calls "the critical example". Here is a boiled down version, much simpler to understand.
module Proxy where
class Dep a b | a -> b instance Dep Char Bool
foo :: forall a. a -> (forall b. Dep a b => a -> b) -> Int foo x f = error "urk"
bar :: (Char -> Bool) -> Int bar g = foo 'c' g
You would think this should be legal, since bar is just an instantation of foo, with a=Char and b=Bool. But GHC rejects it. Why?
Thomas Jäger
I believe there may be some nasty interactions with generalized newtype-deriving, since we can construct two Leibniz-equal types which are mapped to different types using fundeps:
class Foo a where foo :: forall f. f Int -> f a
instance Foo Int where foo = id
newtype Bar = Bar Int deriving Foo
I think this is where your example falls apart. The compiler cannot sensibly derive the instance of Foo for Bar. Why? Because, if written explicitly, its implementation would need to be something like instance Foo Bar where foo = fmap Bar but that is invalid, because the signature is different: foo :: forall f . Functor f => f Int -> f Bar As it happens, the compiler probably does derive some different code for 'foo', namely an unsafe coercion, but it is code that could not be written explicitly by the user. That is why you are able to reveal the coercion via some other route. Regards, Malcolm
participants (4)
-
Iavor Diatchki -
Malcolm Wallace -
Simon Peyton-Jones -
Thomas Jäger