1 Critics and responses

I would like to thank you every feedback given on this reddit entry.
Please give further feedback on the new reddit entry.

Update (17 April) The wrong reference composition problem is solved with an abstract unit type. Now the type system checks the composition law for references.

1.1 Why it depends on data-lens? Why not lens? (donri)

LGtk is built on neither lens nor data-lens. It uses only a handy type class (Tensor) from the data-lens package. I removed the dependency on data-lens anyway.

I have found no description of monadic lenses in existing lens libraries, so I made a new system.
edwardkmett pointed out that I could use fclabels which allows you to inject arbitrary arrows, but fclabel lenses have the quadratic composition problem so I prefer not to use it.

1.2 Monadic lenses have no laws (edwardkmett)

edwardkmett said that he is not against of the particular usage of them in the LGtk API, rather he does not like the idea of their general adoption, because there are no laws for them.

twanvl pointed out that the obvious laws for pure monadic lenses with

getL :: MLens a b -> a -> m b
setL :: MLens a b -> b -> a -> m a


setL l b a >>= getL l          ===  setL l b a >> return b    -- set-get
getL l a >>= \b -> setL l b a  ===  return a                  -- get-set
setL l b a >>= setL l b'       ===  setL l b' a               -- set-set

Indeed, these laws hold for fstLens and fstLens . fstLens for example (fstLens is defined in the package).

I mentioned also the “pure reference laws” (corrected version):

type Ref m a = MLens m () a
readRef r    = getL r ()
writeRef r a = setL r a ()
readRef r >> return ()        ===  return ()
writeRef r a >> readRef r     ===  writeRef r a >> return a
readRef r >>= writeRef r      ===  return ()
writeRef r a >> writeRef r a' ===  writeRef r a'

If we inline the definitions of readRef and writeRef, we get

getL r () >> return ()          ===  return ()               -- specialized get-no-effect
setL r a () >> getL r ()        ===  setL r a () >> return a -- specialized set-get
getL r () >>= \b -> setL r b () ===  return ()               -- specialized get-set
setL r a () >> setL r a' ()     ===  setL r a' ()            -- specialized set-set

so the only new law here is

getL k a >> return ()  ===  return ()    -- get-no-effect

edwardkmett and dcoutts had doubts that the mentioned laws would hold for any of the lenses defined in the API.
They were right, and with a good reason.

edwardkmett highlighted that

newRef :: a -> Ref IO a

will not fulfil any laws with the current implementation in a multi-threaded environment. Even get-no-effect is somewhat problematic in STM, as he said.

There are surprises even in a single-threaded environment. The result of the following computation is 3, not 4!

   r <- newRef 3
   writeRef (r . unitLens . r) 4
   readRef r    -- gives 3

1.2.1 Solution

1.2.2 Conclusion

Monadic lenses do have laws!

1.3 Representation of MLens could be better (edwardkmett)

Right, I already corrected it, I replaced data with newtype in the definition.

edwardkmett would suspect that for this style of lens

data MLens m a b = MLens (a -> m b) (a -> b -> m a)

would be more efficient for many use cases and would avoid spurious read conflicts when you just want to write blindly, as for this kind of lens you are probably more concerned with false serialization for things like MLens STM actions than you are with sharing the traversal down to a given point between the getter and the setter, and you can’t do all the lens tricks to fuse multiple passes together for traversals anyway.

If offers less efficient composition though. I suggested

newtype MLens m a b = MLens (a -> m (m b, b -> m a))

I do not plan to change the representation however, because

I would revisit this issue later if needed.

1.4 Can we reason about impure lenses? (jfischoff)

jfischoff asked whether are there any laws for non-quite lenses.

One of my students is working exactly on this, he constructs formal proofs in Agda about which laws hold for the lenses and which laws are preserved by lens transformations. Stay tuned!

I think that we should allow impure lenses but their laws should be documented.
Consider that if you say like “noncommutative multiplication is not allowed” you lose quaternions. Or if you say “multiplication should be at least associative” you lose octonions. The stricter you are, the more you lose. We should allow everything which helps to write nice code and we should study which laws hold for the constructs we use. If we allow a nonassociative (%) operator for example, we may even code more information into the source: ((a % b) % c) will denote a different intention by the programmer than (a % (b % c)).

1.5 The implementation of Ext leaks memory and time (gereeter)

Correct. I don’t regret because Ext is a pure reference implementation for ExtRef.
An IORef based implementation should have much better performance. I put it into the TODO list.

1.6 The library should be split into two parts (gereeter)

gereeter pointed out that the ExtRefs have nothing to do with GTK specifically, and have other uses.

Agreed, I put the split into the TODO list.

1.7 Why is the description of GUI is parametric over an arbitrary monad when the only interpreter given is for IO? (sclv)

Because in this way we have a chance to test a GUI without running it.

I have changed the type of the interpreter anyway. Now it has type

runI :: (forall m. (Functor m, ExtRef m) => I m) -> IO ()

1.8 More examples (sclv)

sclv wrote: “I’d like to see … perhaps some examples with more interaction between various bits of the structure – i.e. what mechanisms are there for some updates triggering other things in a very non-local way (with regards to structure in an interface) and for some updates to be”bunched up" and only triggered later – i.e. a form is filled out but another part is rendered only on click of a button? A calculator app is a good test-case for these sorts of things, I’ve found."

OK, I a calculator app is now on my TODO list!

1.9 The implementation is not documented (sclv)

Yes, this is on my TODO list.

1.10 No version control

There were no critics about this, but I have created a darcs repo.

Version control starts with lgtk-

2 Summary


TODO list (priorities given by me):

3 Links