Field accessor type inference woes

[Edward Kmett]

On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry <adam.gundry at strath.ac.uk>wrote:

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

My understanding from a recent interaction with Iavor was that the old
difference between functional dependencies and type families where the
fundep only chose the 'instance' rather than the actual meaning of the
arguments has changed recently, to make the two approaches basically
indistinguishable.

This happened as part of the resolution to
http://hackage.haskell.org/trac/ghc/ticket/2247 as I understand it.

In particular this broke similar code that relied on this functionality in
lens and forced a rather large number of patches that had made (ab)use of
the old fundep behavior to be reverted in lens.

Consequently, I don't think you'll find much of a difference between the
type family and the functional depency, except that the latter is forced to
infect more type signatures.

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

Well, it does have the unfortunate consequence that it dooms the lifted
instance we talked about that could make all field accessors automatically
lift into lenses, as that required inference to flow backwards from the
'field' to the 'record'.

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

The awkward part about that is that it becomes impossible to write code
that is polymorphic and have it get the more general signature without
putting dummies in scope just to force conflict.

-Edward


> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130701/d1b97bf2/attachment.htm>