GHC support for the new "record" package

[Edward Kmett]

On Tue, Jan 27, 2015 at 4:07 AM, Adam Gundry <adam at well-typed.com> wrote:
>
> AFAICS it's still an open question as to whether that instance
> should provide
>
> (a) selector functions r -> a
> (b) lenses (a -> f b) -> s -> f t
> (c) both
> (d) neither
>
> but I'm starting to think (b) is the sanest option.
>

Glad I'm not the only voice in the wilderness ;)

On the syntax question, Edward, could you say more about how you would
> expect the magic imports to work? If a module both declares (or imports)
> a record field `x` and magically imports `x`, what does a use of `x`
> mean? (In the original ORF, we didn't have the magic module, but just
> said that record fields were automatically polymorphic... that works but
> is a bit fiddly in the renamer, and isn't a conservative extension.)
>

The straw man I was offering when this was just about {| foo :: .., ... |}
-style records would be to have those bring into scope the Field.foo lenses
by default as a courtesy, since there is nothing involved in that that
necessarily ever defines a normal field accessor.

I'm very much not convinced one way or the other if such a courtesy import
would be better than requiring the user to do it by hand.

It is when we start mixing this with ORF that things get confusing, which
is of course why we're having this nice big discussion.

Having definitions we bring from that module able to be used with normal
records via something like the ORF makes sense. It invites some headaches
though, as higher-rank fields seem to be a somewhat insurmountable obstacle
to the latter, whereas they can be unceremoniously ignored in anonymous
records, since they didn't exist before.

As Neil noted, you _can_ write `foo = @foo` to make such an accessor have
the lighter weight syntax. Of course, once folks start using template
haskell to do so, we get right back to where we are today. It also invites
the question of where such exports should be made.

I'm less sanguine about the proposed IV class, as it doesn't actually work
in its current incarnation in the proposal as mentioned above.

Assuming it has been modified to actually compose and infer, the benefit of
the `import Field (...)` or naked @foo approach is that if two modules
bring in the same field they are both compatible when imported into a third
module.

One half-way serious option might be to have that Field or Lens or whatever
module just export `foo = @foo` definitions from a canonical place so they
can be shared, and to decide if folks have to import it explicitly to use
it.

Then @foo could be the lens to get at the contents of the field, can do
type changing assignment, and users can import the fields to avoid the
noise.

It confess, the solution there feels quite heavy, though.

-Edward

Adam
>
>
> On 27/01/15 00:59, Edward Kmett wrote:
> > I'm also rather worried, looking over the IV proposal, that it just
> > doesn't actually work.
> >
> > We actually tried the code under "Haskell 98 records" back when Gundry
> > first started his proposal and it fell apart when you went to compose
> them.
> >
> > A fundep/class associated type in the class is a stronger constraint
> > that a type equality defined on an individual instance.
> >
> > I don't see how
> >
> > @foo . @bar . @baz
> >
> > (or #foo . #bar . #baz as would be written under the concrete proposal
> > on the wiki)
> >
> > is ever supposed to figure out the intermediate types when working
> > polymorphically in the data type involved.
> >
> > What happens when the type of that chain of accessors is left to
> > inference? You get stuck wallowing in AllowAmbiguousTypes territory:
> >
> > (#foo . #bar . #baz) :: (IV "foo" (c -> d), IV "bar" (b -> c), IV "baz"
> > (a -> b)) => a -> d
> >
> > has a variables 'b' and 'c' that don't occur on the right hand side, and
> > which are only determinable by knowing that the instances you expect to
> > see look something like:
> >
> > instance (a ~ Bool) => IV "x" (S -> a) where
> >   iv (MkS x) = x
> >
> > but that is too weak to figure out that "S" determines "a" unless S is
> > already known, even if we just limit ourselves to field accessors as
> > functions.
> >
> > -Edward
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150127/81428bff/attachment.html>