Hi Edward, I was envisaging that we might well need a functional dependency class Has (r :: *) (x :: Symbol) (t :: *) | r x -> t and, as you point out, composition of polymorphic accessors certainly motivates this. Isn't that enough, though? I think it works out more neatly than the type family version, not least because evidence for a Has constraint is still merely a projection function, and we can still handle universally quantified fields. Obviously it will still not allow determining the type of a record from the type of one of its fields, but that doesn't seem unreasonable to me. Have you any examples where this will be problematic? Moreover, I suggest that Has constraints are only introduced when there are multiple fields with the same name in scope, so existing code (with no ambiguity) will work fine. Thanks, Adam On 01/07/13 15:48, Edward Kmett wrote:
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