[Haskellcafe] Functional dependencies and type inference
Simon PeytonJones
simonpj at microsoft.com
Tue Aug 23 06:36:21 EDT 2005
Thomas
Strange and interesting example! If I had a pound for every time functional dependencies had messed up my brain, I'd be a rich man. Apart from anything else, your example is another case of the "critical example"
http://www.haskell.org/pipermail/haskellcafe/2005August/010974.html
as you mention. It's also jolly strange that GHC infers the (unwritable) type
bar :: (forall r. (Dep Int r) => Int > r) > Bar > Char
but you can write neither that type nor
bar :: (Int > Bool) > Bar > Char
so in fact GHC won't type the bogus typecast. Nevertheless, those are artefacts of GHC's notyetright implementation of fundeps.
I think the real problem here is that the "newtypederiving" mechanism isn't conservative enough. Given
class C a where { op :: ty }
newtype T = MkT S
the idea is that if S is an instance of a class C, then T can be, witnessed by the same functions.
That amounts to saying that
ty[S/a] is interchangeable with ty[T/a]
and that isn't really true when fundeps get in on the act.
I can't say I really understand it fully, but that's as far as I can take it today.
Question: what restrictions on the newtypederiving mechanism would make it sound?
Simon
 Original Message
 From: Thomas Jäger [mailto:thjaeger at gmail.com]
 Sent: 23 August 2005 02:02
 To: Simon PeytonJones
 Cc: Einar Karttunen; haskellcafe at haskell.org
 Subject: Re: [Haskellcafe] Functional dependencies and type inference

 Simon,

 I believe there may be some nasty interactions with generalized
 newtypederiving, since we can construct two Leibnizequal 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 PeytonJones <simonpj at microsoft.com> 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?
More information about the HaskellCafe
mailing list