
On Tue, Jan 27, 2015 at 4:07 AM, Adam Gundry
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
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
On 27/01/15 00:59, Edward Kmett wrote: 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/