Field accessor type inference woes

[Simon Peyton-Jones]

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 at gmail.com]
Sent: 01 July 2013 18:21
To: Adam Gundry
Cc: Simon Peyton-Jones; glasgow-haskell-users at haskell.org
Subject: Re: Field accessor type inference woes

On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry <adam.gundry at strath.ac.uk<mailto: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/20130702/f45275e1/attachment-0001.htm>