GHC support for the new "record" package

[Edward Kmett]

On Tue, Jan 27, 2015 at 6:12 AM, Simon Peyton Jones <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/20150127/082654ce/attachment-0001.html>