Adam, are you willing to update the wiki page to reflect the latest state of the conversation, identifying remaining choices? That would be v helpful. Simon | -----Original Message----- | From: Adam Gundry [mailto:adam@well-typed.com] | Sent: 27 January 2015 09:07 | To: Edward Kmett; Simon Peyton Jones | Cc: Simon Marlow; ghc-devs@haskell.org | Subject: Re: GHC support for the new "record" package | | Yes, we can't make IV the magic class for which instances are | generated. | As I pointed out earlier in the thread, we need to give an instance | for the function space that enforces the functional dependency (either | with an actual fundep or a type family), and keep a distinguished | HasField class. 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. | | Otherwise, I think we've more or less converged on the issues (apart | from the syntax question) and I'll update the wiki page appropriately. | | 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.) | | 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/