donri)edwardkmett)MLens could be better (edwardkmett)jfischoff)Ext leaks memory and time (gereeter)gereeter)sclv)sclv)sclv)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.
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.
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 aare
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-setIndeed, 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 () areadRef 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-setso the only new law here is
getL k a >> return () === return () -- get-no-effectedwardkmett 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 awill 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!
do
r <- newRef 3
writeRef (r . unitLens . r) 4
readRef r -- gives 3(newRef :: a -> Ref IO a) is used only internally by the LGtk implementation.
I added laws to the NewRef type class to recognise bad instances (newRef is a member of this type class).
The LGtk examples use only blessed NewRef instances.
The type signature of the main rendering function runI is changed, so that it does not mention IO now.
twanvl had a remark that “it is safe only to compose with monadic lenses on the right. I.e. to apply a pure lens to the result of a monadic one to get a new monadic lens.”
The wrong reference composition problem is solved with an abstract unit type. The type system checks the composition law for references.
Monadic lenses do have laws!
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
MLens STM (see above).I would revisit this issue later if needed.
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)).
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.
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.
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 ()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!
sclv)Yes, this is on my TODO list.
There were no critics about this, but I have created a darcs repo.
Version control starts with lgtk-0.1.0.2.
Done:
runIunsafe prefix.TODO list (priorities given by me):
ExtRefs and create a new package on HackageDBIORef based ExtRef instance which has no space and time leak