David Turner dct25-561bs at mythic-beasts.com
Tue Jan 27 17:50:44 UTC 2015

```For the record, I think the isomorphism uses the Const s functor to
recover the getter and the Identity functor to recover the setter.
It's something like this:

Given (get, set), the corresponding lens is \f x. fmap (flip set x) (f (get x))
Given a lens ell the getter/setter pair is (runConst . ell Const, \v
-> runIdentity . ell (Identity . const v))

Notice that Const s is not an Applicative (e.g. pure :: () -> Const
Void () doesn't exist) which is why (forall f. Applicative f => (s ->
f s) -> a -> f a) proscribes getting your hands on the getter.

On 27 January 2015 at 17:25, Tom Ellis
> On Tue, Jan 27, 2015 at 05:18:41PM +0000, David Turner wrote:
>> I believe that the types (a -> s, s -> a -> a) and (forall f.  Functor f
>> => (s -> f s) -> a -> f a) are isomorphic.  Is that right?
>
> Yes (with the caveat that I don't actually know how to prove this).
>
>> It's also possible that you can't get the full generality of (forall
>> f. (s -> f t) -> a -> f b) lenses with getter/setter pairs
>
> No, they are equivalent.
>
>> So, my question is: what is the advantage of representing lenses in
>> the way that they are?
>
> The advantage that's most obvious to me is polymorphism.  You can use a lens
>
>     forall f.  Functor f => (s -> f s) -> a -> f a
>
> where the callee expects a traversal
>
>     forall f.  Applicative f => (s -> f s) -> a -> f a
>
> This is very convenient in practice.  Perhaps there are other practical
> advantages that someone else can explain.
>
> Tom
> _______________________________________________