GHC support for the new "record" package

[Dan Doel]

The MPTC solution I was thinking of was similar to the approach one would
take to making arithmetic work like it does in most other languages. I.E.

    class Arithmetic a b c | a b -> c where
      (+) :: a -> b -> c
      ...

One takes that class and then enumerates instances for all combinations of
auto-promotions that should take place.

The And type function is similar to this, although it's cleaner than having
separate types and an MPTC (I think). Maybe it could be made to work, but I
think it's still difficult, and worry that it might never work as well as
what lens currently does.

For instance, when we go to write (.), how do we prove that:

    forall f. (c1 f, c2 f) => (a -> f b) -> s -> f t

(which is what we'll have) is the same type as:

    forall f. And c1 c2 f => (a -> f b) -> s -> f t

(which is what we'll need)?

If we define And by cases, it will not reduce when c1 and c2 are opaque.
But we must define And by cases or it won't be able to reduce things like
'And Applicative Functor' to just 'Applicative' automatically, which is
also important (and we probably wouldn't be able to partially apply it).

We could also define (.) by cases, but then we are back to enumerating all
the combinations of lens-like things, Arithmetic style. And all with
identical implementations.

Perhaps this style solution is acceptable due to lens having a closed set
of interacting types (or does it). But it seems a lot messier at first
blush.

-- Dan

On Wed, Jan 28, 2015 at 5:32 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

>   As soon as you have a distinct Lens type, and use something
> Category-like for composition, you are limiting yourself to composing two
> lenses to get back a lens (barring a terrible mptc 'solution'). And that is
> weak. The only reason I (personally) think lens pulls its weight, and is
> worth using (unlike every prior lens library, which I never bothered with),
> is the ability for lenses, prisms, ismorphisms, traversals, folds, etc. to
> properly degrade to one another and compose automatically.​
>
> Aha.  I keep asking whether it’s just the cute ability to re-use (.) that
> justifies the lack of abstraction in the Lens type.  But Dan’s comment has
> made me remember something from my own talk on the subject.  Here are the
> types of lenses and traversals (2-parameter versions):
>
>
>
> type Lens’      s a = forall f. Functor f
>
>                            => (a -> f a) -> (s -> f s)
>
> type Traversal’ s a = forall f. Applicative f
>
>                            => (a -> f a) -> (s -> f s)
>
>
>
> Suppose we have
>
> ln1 :: Lens'      s1 s2
>
> tr1 :: Traversal' s1 s2
>
> ln2 :: Lens'      s2 a
>
> tr2 :: Traversal' s2 a
>
>
>
> Now these compositions are all well typed
>
> ln1 . ln2 :: Lens' s1 a
>
> tr1 . tr2 :: Traversal' s1 a
>
> tr1 . ln2 :: Traversal' s1 a
>
> ln1 . tr2 :: Traversal' s1 a
>
>
>
> which is quite remarkable.  If Lens’ and Traversal’ were newtypes, you’d
> need four different operators.  (I think that what Dan means by “a terrible
> mptc solution” is trying to overload those four operators into one.)
>
>
>
> I don’t know if this exhausts the reasons that lenses are not abstract.  I
> would love to know more, explained in a smilar style.
>
>
>
> Incidentally has anyone explored this?
>
>
>
> newtype PolyLens c s a = PL (forall f. c f => (a -> f a) -> s -> f s)
>
>
>
> I’ve just abstracted over the Functor/Applicative part, so that Lens’ and
> Traversal’ are both PolyLenses.  Now perhaps we can do (.), with a type like
>
>
>
> (.) :: PolyLens c1 s1 s2 -> PolyLens c2 s2 a -> PolyLens (And c1 c2) s1 a
>
>
>
> where And is a type function
>
>
>
> type instance And Functor Applicative = Applicative
>
> etc
>
>
>
> I have no idea whether this could be made to work out, but it seems like
> an obvious avenue so I wonder if anyone has explored it.
>
>
>
> Simon
>
>
>
> *From:* Dan Doel [mailto:dan.doel at gmail.com]
> *Sent:* 28 January 2015 00:27
> *To:* Edward Kmett
> *Cc:* Simon Peyton Jones; ghc-devs at haskell.org
> *Subject:* Re: GHC support for the new "record" package
>
>
>
> On Tue, Jan 27, 2015 at 6:47 PM, Edward Kmett <ekmett at gmail.com> wrote:
>
>
>
> This works great for lenses that don't let you change types.
>
>
>
> ​This is not the only restriction required for this to be an acceptable
> solution.
>
> As soon as you have a distinct Lens type, and use something Category-like
> for composition, you are limiting yourself to composing two lenses to get
> back a lens (barring a terrible mptc 'solution'). And that is weak. The
> only reason I (personally) think lens pulls its weight, and is worth using
> (unlike every prior lens library, which I never bothered with), is the
> ability for lenses, prisms, ismorphisms, traversals, folds, etc. to
> properly degrade to one another and compose automatically. So if we're
> settling on a nominal Lens type in a proposal, then it is automatically
> only good for one thing to me: defining values of the better lens type.​
>
> -- Dan
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20150128/824189f8/attachment.html>