Re: [Haskell-cafe] Functional dependencies and type inference
Thomas Jäger [EMAIL PROTECTED] writes: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional dependencies and type inference
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 [EMAIL PROTECTED] wrote:
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?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
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: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional dependencies and type inference
Hello, On 8/11/05, Simon Peyton-Jones [EMAIL PROTECTED] wrote: ... 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
