LGtk/Semantics
The semantics of LGtk is given by a reference implementation. The reference implementation is given in three stages: lenses, references and effects. Comments on Reddit
Contents
Lenses
LGtk uses simple lenses defined in the datalens package:
newtype Lens a b = Lens { runLens :: a > Store b a }
This data type is isomorphic to (a > b, b > a > a)
, the wellknow lens data type. The isomorphism is established by the following operations:
getL :: Lens a b > a > b
setL :: Lens a b > b > a > a
lens :: (a > b) > (b > a > a) > Lens a b
Lens laws
The three wellknown laws for lenses:
 getset:
setL k (getL k a) a
===a
 setget:
getL k (setL k b a)
===b
 setset:
setL k b2 (setL k b1 a)
===setL k b2 a
Impure lenses, i.e. lenses which break lens laws are allowed in certain places. Those places are explicitly marked and explained in this overview. (TODO)
References
Motivation
Let s :: *
be a type.
Consider the three types Lens s :: * > *
, State s :: * > *
, Reader s :: * > *
with their type class instances and operations. This rich structure is useful in practice (see this use case).
We have the following goals:
 Define a structure similar to
(Lens s, State s, Reader s)
in whichs
is not accessible.  Extend the defined structure with operations which help modularity.
The first goal is justified by our solution for the second goal. The second goal is justified by the fact that a global state is not convenient to maintain explicitly.
Types
We keep the types (Lens s, State s, Reader s)
but give them a more restricted API. There are several ways to do this in Haskell. LGtk defines type classes with associated types, but that is just a technical detail.
Instead of giving a concrete implementation in Haskell, suppose that

s
is a fixed arbitrary type, 
Ref :: * > *
~Lens s
; references are lenses froms
to the type of the referred value, 
R :: * > *
~Reader s
; the reference reading monad is the reader monad overs
, 
M :: * > *
~State s
; the reference modifying monad is the state monad overs
.
The three equality constraints are not exposed in the API, of course.
Operations
Exposed operations of Ref
, R
and M
are the following:
 The
Monad
instance ofR
andM
 The monad morphism between
R
andM
liftReadPart :: R a > M a
liftReadPart = gets . runReader
 Reference read
readRef :: Ref a > R a
readRef = reader . getL
 Reference write
writeRef :: Ref a > a > M ()
writeRef = modify . setL r
 Lens application on a reference
lensMap :: Lens a b > Ref a > Ref b
lensMap = (.)
 Reference join
joinRef :: R (Ref a) > Ref a
joinRef = Lens . join . (runLens .) . runReader
 The unit reference
unitRef :: Ref ()
unitRef = lens (const ()) (const id)
Note that the identity lens is not a reference because that would leak the program state s
.
Reference laws
Laws for liftReadPart
(derived from the properties of the Reader
monad):

liftReadPart m >> return ()
===return ()

liftM2 (,) (liftReadPart m) (liftReadPart m)
===liftM (\a > (a, a)) (liftReadPart m)
Laws for readRef
and writeRef
(derived from lens laws):

liftReadPart (readRef r) >>= writeRef r
===return ()

writeRef r a >> liftReadPart (readRef r)
===return a

writeRef r a >> writeRef r a'
===writeRef r a'
Laws for lens application:

lensMap id r
===r

lensMap k (lensMap l r)
===lensMap (k . l) r

readRef (lensMap k r)
===liftM (getL k) (readRef r)

writeRef (lensMap k r) a
===liftReadPart (readRef r) >>= writeRef r . setL k a
Laws for reference join:

joinRef (return r)
===r

readRef (joinRef m)
===m >>= readRef

writeRef (joinRef m) a
===liftReadPart m >>= flip writeRef a
Laws for the unit refernce:

readRef unitRef
===return ()
Reference creation
New reference creation is our first operation wich helps modularity.
New reference creation with a given initial value extends the state. For example, if the state is (1, 'c') :: (Int, Char)
, extending the state with True :: Bool
would yield the state (True, (1, 'c')) :: (Bool, (Int, Char))
.
We could model the type change of the state with an indexed monad, but that would complicate both the API and the implementation too.
Instead of changing the type of the state, we use an extensible state, an abstract data type S
with the operations
empty :: S
extend :: a > State S (Lens S a)
such that the following laws hold:

extend v >> return ()
===return ()

extend v >>= liftReadPart . readRef
===return v
The first law sais that extend
has no sideeffect, i.e. extending the state does not change the values of existing references. The second law sais that extending the state with value v
creates a reference with inital value v
.
Question: Is there a data type with such operations?
The answer is yes, but we should guarantee linear usage of the state. The (constructive) existence proof is given in the next section.
Linear usage of state is guaranteed with the above refereces API (check the definitions), which means that we have a solution.
Can this extensible state be implemented efficiently? Although this question is not relevant for the semantics, we will see that there is an efficient implementation with MVar
s (TODO).
Reference creation API
Let S
be an extensible state as specified above.
Let s
= S
in the definition of references.

C :: (* > *) > * > *
~StateT S
, the reference creating monad, is the state monad transformer overS
.
The equality constraint is not exposed in the API. The following functions are exposed:
 New reference creation
newRef :: Monad m => a > C m (Ref a)
newRef = mapStateT (return . runIdentity) . extend
 Lift reference modifying operations
liftMod :: Monad m => M a > C m a
liftMod = mapStateT (return . runIdentity)
 Derived
MonadTrans
instance ofC
to be able to lift operations in them
monad.
Note that C
is parameterized by a monad because in this way it is easier to add other effects later.
Running
The API is completed with the following function:
 Run the reference creation monad
runC :: Monad m => C m a > m a
runC x = runStateT x empty
Dependent reference creation
Motivation
With newRef
the program state can be extended in an independent way (the new state piece is independent from the others). This is not always enough for modular design.
Suppose that we have a reference r :: Ref (Maybe Int)
and we would like to expose an editor of it to the user. The exposed editor would contain a checkbox and an integer entry field. If the checkbox is unchecked, the value of r
should be Nothing
, otherwise it should be Just i
where i
is the value of the entry field.
The problem is that we cannot remember the value of the entry field if the checkbox is unchecked! Dependent reference creation give a nice solution to this problem.
Specification
Suppose that we have an abstract data type S
with the operations
empty :: S
extend' :: Lens S b > Lens a b > a > State S (Lens S a)
such that the following laws hold:
 Law 1:
extend' r k a0 >> return ()
===return ()
 Law 2:
liftM (k .) $ extend' r k a0
===return r
 Law 3:
extend' r k a0 >>= readRef
===readRef r >>= setL k a0
Law 1 sais that extend'
has no sideeffect. Law 2 sais that k
applied on the result of extend' r k a0
behaves as r
. Law 3 defines the initial value of the newly defined reference.
Usage
Law 2 is the most interesting, it sais that we can apply a lens backwards with extend'
. Backward lens application can introduce dependent local state.
Consider the following pure lens:
maybeLens :: Lens (Bool, a) (Maybe a)
maybeLens
= lens (\(b, a) > if b then Just a else Nothing)
(\x (_, a) > maybe (False, a) (\a' > (True, a')) x)
Suppose that we have a reference r :: Lens S (Maybe Int)
. Consider the following operation:
extend' r maybeLens (False, 0)
This operations returns q :: Lens S (Bool, Int)
. If we connect fstLens . q
to a checkbox and sndLens . q
to an integer entry field, we get the expected behaviour as described in the motivation.
extend'
introduces a dependent local state because q
is automatically updated if r
changes (and viceversa).
Backward lens application can solve longstanding problems with application of lenses, see LGtk/ADT_lenses.
Reference creation API (revised)
Let S
be an extensible state as specified above.
Let s
= S
in the definition of references.

C :: (* > *) > * > *
~StateT S
, the reference creating monad, is the state monad transformer overS
.
The equality constraint is not exposed in the API. The following functions are exposed:
 Dependent new reference creation
extRef :: Monad m => Ref b > Lens a b > a > C m (Ref a)
extRef r k = mapStateT (return . runIdentity) . extend' r k
 Lift reference modifying operations
liftWrite :: Monad m => M a > C m a
liftWrite = mapStateT (return . runIdentity)
 Derived
MonadTrans
instance ofC
to be able to lift operations in them
monad.
Note that newRef
can be defined in terms of extRef
so extRef
is more powerful than newRef
:
newRef :: Monad m => a > C m (Ref a)
newRef = extRef unitRef (lens (const ()) (const id))
Existence proof of S
We prove constructively, by giving a reference implementation, that S
exists. With this we also prove that S
defined in the previous section exists because extend
can be defined in terms of extend'
(easy exercise: give the definition).
Overview:
The idea behind the implementation is that S
not only stores a gradually extending state with type (a'', (a', (a, ...))
but also a chain of lenses with type Lens (a'', (a', (a, ...))) (a', (a, ...))
, Lens (a', (a, ...)) (a, ...)
, Lens (a, ...) ...
, ...
.
When a new reference is created, both the state and the lenschain are extended. The dependency between the newly created state part and the old state parts can be encoded into the new lens in the lenschain.
When a previously created reference (i.e. a lens) is accessed with a state after several extensions, a proper prefix of the lenschain makes possible to convert the program state such that it fits the previously created reference.
Reference implementation:
Definition of S
:
type S = [Part]
data Part
= forall a
. Part
{ selfAdjustment :: S > a > a  does not change (static)
, statePart :: a  variable
}
Note that instead of lenses, selfadjusting functions are stored in state parts, which is a simplification in the implementation.
Definition of empty
:
empty :: S
empty = []
Auxiliary defintion: Add a state part and adjust its local state.
snoc :: S > Part > S
s `snoc` Part f a
= s ++ [Part f (f s a)]
Definition of extend'
:
extend' :: Lens S b > Lens a b > a > State S (Lens S a)
extend' r1 r2 a = do
 get number of state parts
n < gets length
 add a properly initialized new state part
modify (`snoc` Part (setL r2 . getL r1) a)
 return a lens which accesses n+1+k state parts (k depends on future extensions)
return $ Lens $ mkStore (setL r1 . getL r2) . splitAt n
mkStore :: (a > S > S) > (S, S) > Store a S
mkStore g (s, Part f a: ps)  (previous state parts, self state part: next state parts)
= store
 set self state part,
 adjust previously added state parts (by g),
 adjust recently added state parts (by readding them with snoc)
(\a > foldl snoc (g a s ++ [Part f (unsafeCoerce a)]) ps)
 get self state part
(unsafeCoerce a)
If the values of S
are used linearly, types will match at runtime so the use of unsafeCoerce
is safe.
Summary
References is a structure with the abstract data types

Ref :: * > *
 reference 
R :: * > *
 reference reading monad 
M :: * > *
 reference modifying monad 
C :: (* > *) > * > *
 reference creating monad transformer
where

R
andM
are monads, 
C
is a monad transformer, 
liftReadPart :: R a > M a
is a monad morphism betweenR
andM
, 
liftMod :: Monad m => M a > C m a
is a monad morphism betweenM
andC m
,
with the operations

unitRef :: Ref ()
 unit reference 
lensMap :: Lens a b > Ref a > Ref b
 lens application on a reference 
joinRef :: R (Ref a) > Ref a
 reference join 
readRef :: Ref a > R a
 reference read 
writeRef :: Ref a > a > M ()
 reference write 
extRef :: Monad m => Ref b > Lens a b > a > C m (Ref a)
 reference creation 
runC :: Monad m => C m a > m a
 running
such that the following laws hold

m >> return ()
===return ()
, for allm :: R a

liftM2 (,) m m
===liftM (\a > (a, a)) m
, for allm :: R a

readRef unitRef
===return ()

lensMap id r
===r

lensMap k (lensMap l r)
===lensMap (k . l) r

readRef (lensMap k r)
===liftM (getL k) (readRef r)

writeRef (lensMap k r) a
===liftReadPart (readRef r) >>= writeRef r . setL k a

joinRef (return r)
===r

readRef (joinRef m)
===m >>= readRef

writeRef (joinRef m) a
===liftReadPart m >>= flip writeRef a

liftReadPart (readRef r) >>= writeRef r
===return ()

writeRef r a >> liftReadPart (readRef r)
===return a

writeRef r a >> writeRef r a'
===writeRef r a'

extRef r k a >> return ()
===return ()

liftM (k .) (extRef r k a)
===return r

extRef r k a >>= liftMod . liftReadPart . readRef
===liftMod (liftReadPart (readRef r >>= setL k a))
Effects
TODO