Field accessor type inference woes

[Adam Gundry]

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