Field accessor type inference woes

Adam Gundry adam.gundry at
Mon Jul 1 19:07:03 CEST 2013

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.



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 =
> 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

More information about the Glasgow-haskell-users mailing list