GHC support for the new "record" package

[Simon Peyton Jones]

Ignoring lenses all together for the moment, I don't see how IV works.

Could you take a look at the current version of https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Redesign

and the give an example of something problematic.  You may well be right, but it’s hard to know without something specific to bite on.

You can make a data type
data Lens s a = Lens (s -> a) (a -> s -> s)

You could, but that would be very different to your lovely lenses today, and it is certainly not what I was suggesting. All I was suggesting was

            newtype Lens s t a b = L { unwrap :: forall f. Functor<http://hackage.haskell.org/package/base-4.7.0.1/docs/Control-Monad.html#t:Functor> f => (a -> f b) -> s -> f t }

Just a wrapper around the precise type you use today.  So presumably anything whatsoever that you can do today, you can also do by saying (unwrap l).

Yes, that means you can’t use ordinary function composition (.) for these wrapped lenses.  I agree that’s a pity.  Perhaps this single point is so important that it justifies breaking abstraction.  But breaking abstractions comes with costs, to error messages, and to future evolution.

Are there other costs to having the abstraction, or is it just (.)?  After all, the lens combinators themselves can wrap and unwrap to their heart’s content; it’s just the clients of the library that we care about here.

Simon

From: Edward Kmett [mailto:ekmett at gmail.com]
Sent: 27 January 2015 23:48
To: Simon Peyton Jones
Cc: Adam Gundry; ghc-devs at haskell.org
Subject: Re: GHC support for the new "record" package

On Tue, Jan 27, 2015 at 6:12 AM, Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> wrote:
|  1. What are the IV instances provided in base? These could give
|  selector functions, lenses, both or neither.

My instinct: just selector functions.  Leave lenses for a lens package.

How do these selectors actually typecheck when composed?

Ignoring lenses all together for the moment, I don't see how IV works.


I still have not understood the argument for lenses being a function rather that a newtype wrapping that function; apart from the (valuable) ability to re-use ordinary (.), which is cute.  Edward has explained this several time, but I have failed to understand.

You can make a data type

data Lens s a = Lens (s -> a) (a -> s -> s)

or

newtype Lens s a = Lens (s -> (a, a -> s))

The latter is basically the approach I used to take in my old data-lens library.

This works great for lenses that don't let you change types.

You can write a Category instance for this notion of lens.

You can make it compose the way functions normally compose (or you can flip the arguments and make it compose the way lenses in the lens library do, here you have an option.)

Now, expand it to let you do type changing assignment.

newtype Lens s t a b = Lens (s -> a) (s -> b -> t)

Now we have 4 arguments, but Category wants 2.

I've punted a way-too-messy aside about why 4 arguments are used to the end. [*]

You can come up with a horrible way in which you can encode a GADT

data Lens :: (*,*) -> (*,*) -> * where
  Lens :: (s -> a) -> (s -> b -> t) -> Lens '(s,t) '(a,b)

but when you go to define

instance Category Lens where
  id = ...

you'd get stuck, because we can't prove that all inhabitants of (*,*) look like '(a,b) for some types a and b.

On the other hand, you can make the data type too big

data Lens :: * -> * -> * where
  Lens :: (s -> a) -> (s -> b -> t) -> Lens (s,t) (a,b)
  Id :: Lens a a

but now you can distinguish too much information, GHC is doing case analysis everywhere, etc.

Performance drops like a stone and it doesn't fit the abstraction.

In short, using a dedicated data type costs you access to (.) for composition or costs you the ability to let the types change.

-Edward

[*] Why 4 arguments?

We can make up our own combinators for putting these things together, but we can't use (.) from the Prelude or even from Control.Category.

There are lots of ways to motivate the 4 argument version:

Logically there are two type families involved the 'inner' family and the 'outer' one and the lens type looks like

outer i is isomorphic to the pair of some 'complement' that doesn't depend on the index i, and some inner i.

outer i <-> (complement, inner i)

We can't talk about such families in Haskell though, we need them to compose by pullback/unification, so we fake it by using two instantiations of the schema

outer i -> (inner i, inner j -> outer j)

which is enough for 99% of the things a user wants to say with a lens or field accessor.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150128/8030070c/attachment-0001.html>