Edward, is quite right. Thank you for pointing this out; I hadn’t fully absorbed the consequences of the three-parameter Has class. This isn’t a fundep-vs-type-function thing; it’s a tradeoff between polymorphism and overloading.
There seem to be two alternatives. I’ll use fundep notation just because it’s better known. Same things happen with functions. Here are two records
data R a = MkR { foo :: a -> a }
data S = MkS { bar :: forall b. b -> b }
Here is Plan A: use fundep (or type function)
class Has r f t | r f -> t where
getFld :: r -> t
instance Has (R a) “foo” (a -> a) where ..
instance Has S “bar” (forall b. b -> b) where ...
Lacking (as we still do) impredicative polymorphism, the S instance declaration is rejected.
Here is Plan B: no fundep (or type functions)
class Has r f t where
getFld :: r -> t
instance (t ~ a->a) => Has (R a) “foo” t where ..
instance (t ~ b->b) => Has S “bar” t where ...
Now the instance for S works fine. But the ambiguity problem that Edward describes shows up.
Can you combine A and B?
class Has r f t | r f -> t where
getFld :: r -> t
instance (t ~ b->b) => Has S “bar” t where ...
No: the instance is rejected because the S does not “cover” the free type variable t. This is #2247 I think. There is a good reason for this (I could elaborate if reqd).
Notice too that with
data T = MkT { wib :: (forall b. b -> b) -> Int }
the polymorphic type is more deeply buried, and Plan B doesn’t work either. So Plan B is already a bit of a sticking plaster.
Bottom line: there is a real tension here.
Let’s review the goal:
to allow you to use the same field name in different records.
The current proposal allows you to write
f :: r { foo :: Int } => r -> Int -> Int
which will work on any record with an Int-valued foo field. BUT writing functions like this was never a goal! We could restrict the proposal: we could simply *not abstract* over Has constraints, preventing you from writing ‘f’, but also preventing you from falling over Edward’s problem. (But it would also be an odd restriction, given that Has is in most ways an ordinary class.)
So I think Plan B (the one we are currently proposing) works just fine for the declared goal. We just have to acknowledge that it doesn’t do everything you might possibly want.
Simon
From: Edward Kmett [mailto:ekmett@gmail.com]
Sent: 01 July 2013 18:21
To: Adam Gundry
Cc: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
Subject: Re: Field accessor type inference woes
On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry
It strikes me that there is a fairly major issue with the record proposal as it stands.
Right now the class
class Has (r :: *) (x :: Symbol) (t :: *)
can be viewed as morally equivalent to having several classes
class Foo a b where foo :: a -> b
class Bar a b where bar :: a -> b
for different fields foo, bar, etc.
I'll proceed with those instead because it makes it easier to show the issue today.
When we go to compose those field accessors, you very quickly run into a problem due to a lack of functional dependencies:
When you go to define
fooBar = foo.bar
which is perfectly cromulent with existing record field accessors you get a big problem.
fooBar :: (Foo b c, Bar a b) => a -> c
The b that should occur in the signature isn't on the right hand side, and isn't being forced by any fundeps, so fooBar simply can't be written.
Could not deduce (Foo b0 c) arising from a use of `foo' from the context (Bar a b, Foo b c)
If you leave off the signature you'll get an ambiguity check error:
Could not deduce (Foo b0 c) arising from the ambiguity check for `fooBar' from the context (Bar a b, Foo b c) bound by the inferred type for `fooBar': (Bar a b, Foo b c) => a -> c
It strikes me that punting all functional dependencies in the record types to the use of equality constraints has proven insufficient to tackle this problem. You may be able to bandaid over it by including a functional dependency/type family
class Has (r :: *) (x :: Symbol) where type Got r x :: * getFld :: r -> Got r x
(or to avoid the need for type applications in the first place!)
class Has (r :: *) (x :: Symbol) where type Got r x :: * getFld :: p x -> r -> Got r x
This has some annoying consequences though. Type inference can still only flow one way through it, unlike the existing record accessors, and it would cost the ability to 'cheat' and still define 'Has' for universally quantified fields that we might have been able to do with the proposal as it stands.
-Edward