GHC support for the new "record" package

[Simon Peyton Jones]

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 at well-typed.com]
|  Sent: 27 January 2015 09:07
|  To: Edward Kmett; Simon Peyton Jones
|  Cc: Simon Marlow; ghc-devs at 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/