On Wed, Jan 21, 2015 at 1:06 PM, Adam Gundry <adam@well-typed.com> wrote:

Also, I'd add fields with higher-rank types to the list of missing
features. From a user's perspective, it might seem a bit odd if

data T = MkT { foo :: forall a . a }

was fine but

data T = MkT {| foo :: forall a . a |}

would not be a valid declaration. (Of course, ORF can't overload "foo"
either, and maybe this is an inevitable wart.)

I'm slowly coming around to thinking that this is inevitable without a bunch of changes in the way we work with classes. You otherwise need to allow impredicative types in some contexts, which raises all sorts of questions.

In the latter case we can at least be clear about why it doesn't work in the error message, in the ORF case it has to just not generate a lens. =(

>> 5) I don't know if I want to commit the *language* to a particular lens
>> type.

Agreed, but I don't think this need be an issue for either proposal. We
know from ORF that we can make fields sufficiently polymorphic to be
treated as selector functions or arbitrary types of lenses (though
treating them as van Laarhoven lenses requires either some clever
typeclass trickery in the base library, or using a combinator to make a
field into a lens at use sites).

Admittedly that has also been the source of 90% of the complexity of the ORF proposal. There we _had_ to do this in order to support the use as a regular function.

There is a large design space here, and the main thing Nikita's proposal brings to the table is slightly different assumptions about what such records should mean. This _could_ let us shed some of the rougher edges of ORF, at the price of having to lock in a notion of lenses.

I'm on the fence about whether it would be a good idea to burden Nikita's proposal in the same fashion, but I think it'd be wise to explore it in both fashions. My gut feeling though is that if we tie it up with the same restrictions as ORF you just mostly get a less useful ORF with anonymous record sugar thrown in.

-Edward