LGtk/Semantics
From HaskellWiki
m (→Motivation) 
(add a link) 

(32 intermediate revisions by 2 users not shown)  
Line 1:  Line 1:  
The semantics of LGtk is given by a reference implementation. 
The semantics of LGtk is given by a reference implementation. 

−  The reference implementation is given in three stages: lenses, references and effects. 
+  The reference implementation is given in three stages: lenses, references and effects. [http://www.reddit.com/r/haskell/comments/1fjerf/lens_chains_lgtk_semantics_first_part/ Comments on Reddit] 
== Lenses == 
== Lenses == 

Line 28:  Line 28:  
The three wellknown laws for lenses: 
The three wellknown laws for lenses: 

−  * getset: <hask>set k (get k a) a</hask> === <hask>a</hask> 
+  * getset: <hask>setL k (getL k a) a</hask> === <hask>a</hask> 
−  * setget: <hask>get k (set k b a)</hask> === <hask>b</hask> 
+  * setget: <hask>getL k (setL k b a)</hask> === <hask>b</hask> 
−  * setset: <hask>set k b2 (set k b1 a)</hask> === <hask>set k b2 a</hask> 
+  * setset: <hask>setL k b2 (setL k b1 a)</hask> === <hask>setL k b2 a</hask> 
Impure lenses, i.e. lenses which 
Impure lenses, i.e. lenses which 

−  brake lens laws are allowed in certain places. Those places are explicitly marked and explained in this overview. (TODO) 
+  break lens laws are allowed in certain places. Those places are explicitly marked and explained in this overview. (TODO) 
== References == 
== References == 

Line 41:  Line 41:  
Let <hask>s :: *</hask> be a type. 
Let <hask>s :: *</hask> be a type. 

−  Consider the three types <hask>Lens s :: * > *</hask>, <hask>State s :: * > *</hask>, <hask>Reader s :: * > *</hask> with their type class instances and operations. This structure is useful in practice ([http://www.haskellforall.com/2013/05/programimperativelyusinghaskell.html see this use case]). 
+  Consider the three types <hask>Lens s :: * > *</hask>, <hask>State s :: * > *</hask>, <hask>Reader s :: * > *</hask> with their type class instances and operations. This rich structure is useful in practice ([http://www.haskellforall.com/2013/05/programimperativelyusinghaskell.html see this use case]). 
We have the following goals: 
We have the following goals: 

Line 112:  Line 112:  
Note that the identity lens is '''not''' a reference because that would leak the program state <hask>s</hask>. 
Note that the identity lens is '''not''' a reference because that would leak the program state <hask>s</hask>. 

+  
+  ==== Reference laws ==== 

+  
+  Laws for <hask>liftReadPart</hask> (derived from the properties of the <hask>Reader</hask> monad): 

+  
+  * <hask>liftReadPart m >> return ()</hask> === <hask>return ()</hask> 

+  
+  * <hask>liftM2 (,) (liftReadPart m) (liftReadPart m)</hask> === <hask>liftM (\a > (a, a)) (liftReadPart m)</hask> 

+  
+  Laws for <hask>readRef</hask> and <hask>writeRef</hask> (derived from lens laws): 

+  
+  * <hask>liftReadPart (readRef r) >>= writeRef r</hask> === <hask>return ()</hask> 

+  
+  * <hask>writeRef r a >> liftReadPart (readRef r)</hask> === <hask>return a</hask> 

+  
+  * <hask>writeRef r a >> writeRef r a'</hask> === <hask>writeRef r a'</hask> 

+  
+  Laws for lens application: 

+  
+  * <hask>lensMap id r</hask> === <hask>r</hask> 

+  
+  * <hask>lensMap k (lensMap l r)</hask> === <hask>lensMap (k . l) r</hask> 

+  
+  * <hask>readRef (lensMap k r)</hask> === <hask>liftM (getL k) (readRef r)</hask> 

+  
+  * <hask>writeRef (lensMap k r) a</hask> === <hask>liftReadPart (readRef r) >>= writeRef r . setL k a</hask> 

+  
+  Laws for reference join: 

+  
+  * <hask>joinRef (return r)</hask> === <hask>r</hask> 

+  
+  * <hask>readRef (joinRef m)</hask> === <hask>m >>= readRef</hask> 

+  
+  * <hask>writeRef (joinRef m) a</hask> === <hask>liftReadPart m >>= flip writeRef a</hask> 

+  
+  Laws for the unit refernce: 

+  
+  * <hask>readRef unitRef</hask> === <hask>return ()</hask> 

=== Reference creation === 
=== Reference creation === 

Line 167:  Line 205:  
<haskell> 
<haskell> 

−  liftWrite :: Monad m => M a > C m a 
+  liftMod :: Monad m => M a > C m a 
−  liftWrite = mapStateT (return . runIdentity) 
+  liftMod = mapStateT (return . runIdentity) 
</haskell> 
</haskell> 

Line 186:  Line 224:  
</haskell> 
</haskell> 

−  === Lenschains === 
+  === Dependent reference creation === 
==== Motivation ==== 
==== Motivation ==== 

Line 194:  Line 232:  
Suppose that we have a reference <hask>r :: Ref (Maybe Int)</hask> 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 <hask>r</hask> should be <hask>Nothing</hask>, otherwise it should be <hask>Just i</hask> where <hask>i</hask> is the value of the entry field. 
Suppose that we have a reference <hask>r :: Ref (Maybe Int)</hask> 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 <hask>r</hask> should be <hask>Nothing</hask>, otherwise it should be <hask>Just i</hask> where <hask>i</hask> 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! Lenschains give a nice solution to this problem. 
+  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. 
−  ==== Lowlevel API ==== 
+  ==== Specification ==== 
−  Let's begin with the API. Suppose that we have an abstract data type <hask>S</hask> with the following operations: 
+  Suppose that we have an abstract data type <hask>S</hask> with the operations 
<haskell> 
<haskell> 

Line 235:  Line 273:  
<hask>extend' r maybeLens (False, 0)</hask> 
<hask>extend' r maybeLens (False, 0)</hask> 

−  This operations returns <hask>q :: Lens S (Bool, Int)</hask>. If we connect <hask>fstLens q</hask> to a checkbox and <hask>sndLens q</hask> to an integer entry field, we get the expected behaviour as described in the motivation. 
+  This operations returns <hask>q :: Lens S (Bool, Int)</hask>. If we connect <hask>fstLens . q</hask> to a checkbox and <hask>sndLens . q</hask> to an integer entry field, we get the expected behaviour as described in the motivation. 
<hask>extend'</hask> introduces a dependent local state because <hask>q</hask> is automatically updated if <hask>r</hask> changes (and viceversa). 
<hask>extend'</hask> introduces a dependent local state because <hask>q</hask> is automatically updated if <hask>r</hask> changes (and viceversa). 

−  Backward lens application can solve several longstanding problems with application of lenses, but it is another story to show that. 
+  Backward lens application can solve longstanding problems with application of lenses, see [[LGtk/ADT_lenses]]. 
−  ==== References API ==== 
+  ==== Reference creation API (revised) ==== 
Let <hask>S</hask> be an extensible state as specified above. 
Let <hask>S</hask> be an extensible state as specified above. 

Line 255:  Line 293:  
<haskell> 
<haskell> 

extRef :: Monad m => Ref b > Lens a b > a > C m (Ref a) 
extRef :: Monad m => Ref b > Lens a b > a > C m (Ref a) 

−  extRef r k a0 = mapStateT (return . runIdentity) $ extend' r k a0 
+  extRef r k = mapStateT (return . runIdentity) . extend' r k 
</haskell> 
</haskell> 

Line 267:  Line 305:  
* Derived <hask>MonadTrans</hask> instance of <hask>C</hask> to be able to lift operations in the <hask>m</hask> monad. 
* Derived <hask>MonadTrans</hask> instance of <hask>C</hask> to be able to lift operations in the <hask>m</hask> monad. 

−  Note that <hask>newRef</hask> can be defined in terms of <hask>extRef</hask> so <hask>extRef</hask> is more expressive than <hask>newRef</hask>: 
+  Note that <hask>newRef</hask> can be defined in terms of <hask>extRef</hask> so <hask>extRef</hask> is more powerful than <hask>newRef</hask>: 
<haskell> 
<haskell> 

Line 274:  Line 312:  
</haskell> 
</haskell> 

−  +  ==== Existence proof of <hask>S</hask> ==== 

−  ==== Implementation ==== 

We prove constructively, by giving a reference implementation, that <hask>S</hask> exists. With this we also prove that <hask>S</hask> defined in the previous section exists because <hask>extend</hask> can be defined in terms of <hask>extend'</hask> (easy exercise: give the definition). 
We prove constructively, by giving a reference implementation, that <hask>S</hask> exists. With this we also prove that <hask>S</hask> defined in the previous section exists because <hask>extend</hask> can be defined in terms of <hask>extend'</hask> (easy exercise: give the definition). 

Line 280:  Line 318:  
Overview: 
Overview: 

−  The idea behind the implementation is that <hask>S</hask> not only stores a gradually extending state with type <hask>(a'', (a', (a, ...))</hask> but also a chain of lenses with type <hask>Lens (a'', (a', (a, ...))) (a', (a, ...))</hask>, <hask>Lens (a', (a, ...)) (a, ...)</hask>, <hask>...</hask>. 
+  The idea behind the implementation is that <hask>S</hask> not only stores a gradually extending state with type <hask>(a'', (a', (a, ...))</hask> but also a chain of lenses with type <hask>Lens (a'', (a', (a, ...))) (a', (a, ...))</hask>, <hask>Lens (a', (a, ...)) (a, ...)</hask>, <hask>Lens (a, ...) ...</hask>, <hask>...</hask>. 
−  When a new reference is created, both the state and the lenschain is extended. The depencency information between the newly created state part and the old state parts can be encoded into the new lens in the lenschain. 
+  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 new state such that it fits the previously created reference. 
+  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: 
Reference implementation: 

−  Let <hask>Chain a b</hask> be the type of '''lenschains''', the lists of lenses where neighbouring lenses can be composed (the domain of each lens matches the codomain of the previous lens), the domain of the first lens is <hask>a</hask> and the codomain of the last lens is <hask>b</hask>. 
+  Definition of <hask>S</hask>: 
−  
−  Suppose that we have the following auxiliary functions: 

<haskell> 
<haskell> 

−  chainToLens :: Chain a b > Lens a b 
+  type S = [Part] 
</haskell> 
</haskell> 

<haskell> 
<haskell> 

−  emptyChain :: Chain a a 
+  data Part 
+  = forall a 

+  . Part 

+  { selfAdjustment :: S > a > a  does not change (static) 

+  , statePart :: a  variable 

+  } 

</haskell> 
</haskell> 

+  
+  Note that instead of lenses, selfadjusting functions are stored in state parts, which is a simplification in the implementation. 

+  
+  Definition of <hask>empty</hask>: 

<haskell> 
<haskell> 

−  chainCons :: Lens a b > Chain b c > Chain a c 
+  empty :: S 
+  empty = [] 

</haskell> 
</haskell> 

+  
+  Auxiliary defintion: Add a state part and adjust its local state. 

<haskell> 
<haskell> 

−  chainLength :: Chain a b > Int 
+  snoc :: S > Part > S 
+  s `snoc` Part f a 

+  = s ++ [Part f (f s a)] 

</haskell> 
</haskell> 

−  The definition of <hask>S</hask> (an existentional type): 
+  Definition of <hask>extend'</hask>: 
<haskell> 
<haskell> 

−  type S = forall a 
+  extend' :: Lens S b > Lens a b > a > State S (Lens S a) 
−  . S { value :: a 
+  extend' r1 r2 a = do 
−  , chain :: Chain a () 
+   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 

</haskell> 
</haskell> 

−  
−  Definition of <hask>empty</hask>: 

<haskell> 
<haskell> 

−  empty :: S 
+  mkStore :: (a > S > S) > (S, S) > Store a S 
−  empty = S () emptyChain 
+  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) 

</haskell> 
</haskell> 

−  Definition of <hask>extend'</hask>: 
+  If the values of <hask>S</hask> are used linearly, types will match at runtime so the use of <hask>unsafeCoerce</hask> is safe. 
−  <haskell> 
+  === Summary === 
−  extend' :: Lens S b > Lens a b > a > State S (Lens S a) 

−  extend' r1 r2 a0 = state f where 

−  r21 = setL r1 . getL r2 
+  '''References''' is a structure with the abstract data types 
−  r12 = setL r2 . getL r1 

−  f x0@(S value0 chain0) 
+  * <hask>Ref :: * > *</hask>  reference 
−  = ( k' . chainToLens (takeChain (length chain  length chain0) chain) 
+  * <hask>R :: * > *</hask>  reference reading monad 
−  , S (r12 x0 a0, value0) (chainCons k chain0) 
+  * <hask>M :: * > *</hask>  reference modifying monad 
−  ) 
+  * <hask>C :: (* > *) > * > *</hask>  reference creating monad transformer 
−  where 

−  k = lens snd $ \x (a, _) > (r12 x a, x) 

−  k' = lens fst $ \a (_, x) > (a, r21 a x) 

−  takeChain :: Int > Chain a b > Chain a ? 
+  where 
−  </haskell> 
+  
+  * <hask>R</hask> and <hask>M</hask> are monads, 

+  * <hask>C</hask> is a monad transformer, 

+  * <hask>liftReadPart :: R a > M a</hask> is a monad morphism between <hask>R</hask> and <hask>M</hask>, 

+  * <hask>liftMod :: Monad m => M a > C m a</hask> is a monad morphism between <hask>M</hask> and <hask>C m</hask>, 

+  
+  with the operations 

+  
+  * <hask>unitRef :: Ref ()</hask>  unit reference 

+  * <hask>lensMap :: Lens a b > Ref a > Ref b</hask>  lens application on a reference 

+  * <hask>joinRef :: R (Ref a) > Ref a</hask>  reference join 

+  * <hask>readRef :: Ref a > R a</hask>  reference read 

+  * <hask>writeRef :: Ref a > a > M ()</hask>  reference write 

+  * <hask>extRef :: Monad m => Ref b > Lens a b > a > C m (Ref a)</hask>  reference creation 

+  * <hask>runC :: Monad m => C m a > m a</hask>  running 

+  
+  such that the following laws hold 

+  
+  * <hask>m >> return ()</hask> === <hask>return ()</hask>, for all <hask>m :: R a</hask> 

+  * <hask>liftM2 (,) m m</hask> === <hask>liftM (\a > (a, a)) m</hask>, for all <hask>m :: R a</hask> 

+  
+  * <hask>readRef unitRef</hask> === <hask>return ()</hask> 

+  
+  * <hask>lensMap id r</hask> === <hask>r</hask> 

+  * <hask>lensMap k (lensMap l r)</hask> === <hask>lensMap (k . l) r</hask> 

+  * <hask>readRef (lensMap k r)</hask> === <hask>liftM (getL k) (readRef r)</hask> 

+  * <hask>writeRef (lensMap k r) a</hask> === <hask>liftReadPart (readRef r) >>= writeRef r . setL k a</hask> 

+  
+  * <hask>joinRef (return r)</hask> === <hask>r</hask> 

+  * <hask>readRef (joinRef m)</hask> === <hask>m >>= readRef</hask> 

+  * <hask>writeRef (joinRef m) a</hask> === <hask>liftReadPart m >>= flip writeRef a</hask> 

+  
+  * <hask>liftReadPart (readRef r) >>= writeRef r</hask> === <hask>return ()</hask> 

+  * <hask>writeRef r a >> liftReadPart (readRef r)</hask> === <hask>return a</hask> 

+  * <hask>writeRef r a >> writeRef r a'</hask> === <hask>writeRef r a'</hask> 

−  The code does not compile because <hask>takeChain</hask> is not defined. <hask>takeChain</hask> cannot be given a proper type in this context. However, if we suppose that values of <hask>S</hask> are used linearly, types will match at runtime with the naive implementation of <hask>takeChain</hask>. This means that <hask>unsafeCoerce</hask> can be used safely to force the Haskell compiler to accept the code. 
+  * <hask>extRef r k a >> return ()</hask> === <hask>return ()</hask> 
+  * <hask>liftM (k .) (extRef r k a)</hask> === <hask>return r</hask> 

+  * <hask>extRef r k a >>= liftMod . liftReadPart . readRef</hask> === <hask>liftMod (liftReadPart (readRef r >>= setL k a))</hask> 

== Effects == 
== Effects == 
Latest revision as of 23:00, 7 June 2013
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 
[edit] 1 Lenses
LGtk uses simple lenses defined in the datalens package:
newtype Lens a b = Lens { runLens :: a > Store b a }
getL :: Lens a b > a > b
setL :: Lens a b > b > a > a
lens :: (a > b) > (b > a > a) > Lens a b
[edit] 1.1 Lens laws
The three wellknown laws for lenses:
 getset: ===setL k (getL k a) aa
 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)
[edit] 2 References
[edit] 2.1 Motivation
LetWe have the following goals:
 Define a structure similar to in which(Lens s, State s, Reader s)is not accessible.s
 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.
[edit] 2.2 Types
We keep the typesInstead of giving a concrete implementation in Haskell, suppose that
 is a fixed arbitrary type,s
 ~Ref :: * > *; references are lenses fromLens sto the type of the referred value,s
 ~R :: * > *; the reference reading monad is the reader monad overReader s,s
 ~M :: * > *; the reference modifying monad is the state monad overState s.s
The three equality constraints are not exposed in the API, of course.
[edit] 2.3 Operations
Exposed operations of The instance ofMonadandRM
 The monad morphism between andRM
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)
[edit] 2.3.1 Reference laws
Laws for ===liftReadPart m >> return ()return ()
 ===liftM2 (,) (liftReadPart m) (liftReadPart m)liftM (\a > (a, a)) (liftReadPart m)
 ===liftReadPart (readRef r) >>= writeRef rreturn ()
 ===writeRef r a >> liftReadPart (readRef r)return a
 ===writeRef r a >> writeRef r a'writeRef r a'
Laws for lens application:
 ===lensMap id rr
 ===lensMap k (lensMap l r)lensMap (k . l) r
 ===readRef (lensMap k r)liftM (getL k) (readRef r)
 ===writeRef (lensMap k r) aliftReadPart (readRef r) >>= writeRef r . setL k a
Laws for reference join:
 ===joinRef (return r)r
 ===readRef (joinRef m)m >>= readRef
 ===writeRef (joinRef m) aliftReadPart m >>= flip writeRef a
Laws for the unit refernce:
 ===readRef unitRefreturn ()
[edit] 2.4 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 isWe 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 typeempty :: S
extend :: a > State S (Lens S a)
such that the following laws hold:
 ===extend v >> return ()return ()
 ===extend v >>= liftReadPart . readRefreturn 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[edit] 2.4.1 Reference creation API
Let ~C :: (* > *) > * > *, the reference creating monad, is the state monad transformer overStateT S.S
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 instance ofMonadTransto be able to lift operations in theCmonad.m
[edit] 2.5 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
[edit] 2.6 Dependent reference creation
[edit] 2.6.1 Motivation
WithThe 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.
[edit] 2.6.2 Specification
Suppose that we have an abstract data typeempty :: 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 a0return r
 Law 3: ===extend' r k a0 >>= readRefreadRef r >>= setL k a0
[edit] 2.6.3 Usage
Law 2 is the most interesting, it sais that we can apply a lens backwards withConsider 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)
Backward lens application can solve longstanding problems with application of lenses, see LGtk/ADT_lenses.
[edit] 2.6.4 Reference creation API (revised)
Let ~C :: (* > *) > * > *, the reference creating monad, is the state monad transformer overStateT S.S
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 instance ofMonadTransto be able to lift operations in theCmonad.m
newRef :: Monad m => a > C m (Ref a) newRef = extRef unitRef (lens (const ()) (const id))
[edit] 2.6.5 Existence proof of S
We prove constructively, by giving a reference implementation, that Overview:
The idea behind the implementation is thatWhen 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:
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 ofempty :: 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)]
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)
[edit] 2.7 Summary
References is a structure with the abstract data types
  referenceRef :: * > *
  reference reading monadR :: * > *
  reference modifying monadM :: * > *
  reference creating monad transformerC :: (* > *) > * > *
where
 andRare monads,M
 is a monad transformer,C
 is a monad morphism betweenliftReadPart :: R a > M aandR,M
 is a monad morphism betweenliftMod :: Monad m => M a > C m aandM,C m
with the operations
  unit referenceunitRef :: Ref ()
  lens application on a referencelensMap :: Lens a b > Ref a > Ref b
  reference joinjoinRef :: R (Ref a) > Ref a
  reference readreadRef :: Ref a > R a
  reference writewriteRef :: Ref a > a > M ()
  reference creationextRef :: Monad m => Ref b > Lens a b > a > C m (Ref a)
  runningrunC :: Monad m => C m a > m a
such that the following laws hold
 ===m >> return (), for allreturn ()m :: R a
 ===liftM2 (,) m m, for allliftM (\a > (a, a)) mm :: R a
 ===readRef unitRefreturn ()
 ===lensMap id rr
 ===lensMap k (lensMap l r)lensMap (k . l) r
 ===readRef (lensMap k r)liftM (getL k) (readRef r)
 ===writeRef (lensMap k r) aliftReadPart (readRef r) >>= writeRef r . setL k a
 ===joinRef (return r)r
 ===readRef (joinRef m)m >>= readRef
 ===writeRef (joinRef m) aliftReadPart m >>= flip writeRef a
 ===liftReadPart (readRef r) >>= writeRef rreturn ()
 ===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 . readRefliftMod (liftReadPart (readRef r >>= setL k a))
[edit] 3 Effects
TODO