Personal tools

LGtk/Semantics

From HaskellWiki

< LGtk(Difference between revisions)
Jump to: navigation, search
(complete rewrite of the implementation)
(add a link)
 
(17 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 33: Line 33:
   
 
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/program-imperatively-using-haskell.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/program-imperatively-using-haskell.html see this use case]).
   
 
We have the following goals:
 
We have the following goals:
Line 115: Line 115:
 
==== Reference laws ====
 
==== Reference laws ====
   
From lens laws we can derive the following 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>liftReadPart (readRef r) >>= writeRef r</hask> === <hask>return ()</hask>
Line 123: Line 123:
 
* <hask>writeRef r a >> writeRef r a'</hask> === <hask>writeRef r a'</hask>
 
* <hask>writeRef r a >> writeRef r a'</hask> === <hask>writeRef r a'</hask>
   
Additional laws derived from the properties of the <hask>Reader</hask> monad:
+
Laws for lens application:
   
* <hask>liftReadPart m >> return ()</hask> === <hask>return ()</hask>
+
* <hask>lensMap id r</hask> === <hask>r</hask>
   
* <hask>liftM2 (,) (liftReadPart m) (liftReadPart m)</hask> === <hask>liftM (\a -> (a, a)) (liftReadPart m)</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 183: Line 183:
   
 
<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 202: Line 202:
 
</haskell>
 
</haskell>
   
=== Lens-chains ===
+
=== Dependent reference creation ===
   
 
==== Motivation ====
 
==== Motivation ====
Line 210: Line 210:
 
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! Lens-chains 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.
   
==== Low-level 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 255: Line 255:
 
<hask>extend'</hask> introduces a dependent local state because <hask>q</hask> is automatically updated if <hask>r</hask> changes (and vice-versa).
 
<hask>extend'</hask> introduces a dependent local state because <hask>q</hask> is automatically updated if <hask>r</hask> changes (and vice-versa).
   
Backward lens application can solve long-standing problems with application of lenses, but that is another story to tell.
+
Backward lens application can solve long-standing 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 271: Line 271:
 
<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 283: Line 283:
 
* 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 290: Line 290:
 
</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 298: Line 298:
 
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>.
 
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 lens-chain are extended. The depencency information between the newly created state part and the old state parts can be encoded into the new lens in the lens-chain.
+
When a new reference is created, both the state and the lens-chain are extended. The dependency between the newly created state part and the old state parts can be encoded into the new lens in the lens-chain.
   
 
When a previously created reference (i.e. a lens) is accessed with a state after several extensions, a proper prefix of the lens-chain makes possible to convert the program 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 lens-chain makes possible to convert the program state such that it fits the previously created reference.
Line 312: Line 312:
   
 
<haskell>
 
<haskell>
data Part = forall a . Part (S -> a -> 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, just set functions are stored, a simplification in the implementation.
+
Note that instead of lenses, self-adjusting functions are stored in state parts, which is a simplification in the implementation.
   
 
Definition of <hask>empty</hask>:
 
Definition of <hask>empty</hask>:
Line 324: Line 324:
 
</haskell>
 
</haskell>
   
Auxiliary defintions:
+
Auxiliary defintion: Add a state part and adjust its local state.
   
 
<haskell>
 
<haskell>
app :: S -> Part -> Part
+
snoc :: S -> Part -> S
app s (Part f a) = Part f (f s a)
+
s `snoc` Part f a
</haskell>
+
= s ++ [Part f (f s a)]
 
<haskell>
 
snoc :: Part -> S -> S
 
x `snoc` xs = xs ++ [x]
 
 
</haskell>
 
</haskell>
   
Line 336: Line 336:
 
<haskell>
 
<haskell>
 
extend' :: Lens S b -> Lens a b -> a -> State S (Lens S a)
 
extend' :: Lens S b -> Lens a b -> a -> State S (Lens S a)
extend' r1 r2 a0 = state f where
+
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
  +
</haskell>
   
r21 = setL r1 . getL r2
+
<haskell>
r12 = setL r2 . getL r1
+
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 re-adding them with snoc)
  +
(\a -> foldl snoc (g a s ++ [Part f (unsafeCoerce a)]) ps)
  +
-- get self state part
  +
(unsafeCoerce a)
  +
</haskell>
   
f x0 = (lens get set, Part r12 (r12 x0 a0) `snoc` x0)
+
If the values of <hask>S</hask> are used linearly, types will match at runtime so the use of <hask>unsafeCoerce</hask> is safe.
where
 
n = length x0
 
   
get = (\(Part _ a) -> unsafeCoerce a) . (!! n)
+
=== Summary ===
   
set a x = foldl (\s -> (`snoc` s) . app s)
+
'''References''' is a structure with the abstract data types
(Part r12 a `snoc` r21 a (take n x))
 
(drop (n+1) x)
 
</haskell>
 
   
There are two sublte points in the implementation: the usage of <hask>unsafeCoerce</hask> and <hask>(!!)</hask>.
+
* <hask>Ref :: * -> *</hask> -- reference
  +
* <hask>R :: * -> *</hask> -- reference reading monad
  +
* <hask>M :: * -> *</hask> -- reference modifying monad
  +
* <hask>C :: (* -> *) -> * -> *</hask> -- reference creating monad transformer
  +
  +
where
  +
  +
* <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>
   
If the values of <hask>S</hask> are used linearly, <hask>(!!)</hask> never fails and types will match at runtime so the use of <hask>unsafeCoerce</hask> is safe.
+
* <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 data-lens package:

newtype Lens a b = Lens { runLens :: a -> Store b a }
This data type is isomorphic to
(a -> b, b -> a -> a)
, the well-know 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

[edit] 1.1 Lens laws

The three well-known laws for lenses:

  • get-set:
    setL k (getL k a) a
    ===
    a
  • set-get:
    getL k (setL k b a)
    ===
    b
  • set-set:
    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

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 which
    s
    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.

[edit] 2.2 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 from
    s
    to the type of the referred value,
  • R :: * -> *
    ~
    Reader s
    ; the reference reading monad is the reader monad over
    s
    ,
  • M :: * -> *
    ~
    State s
    ; the reference modifying monad is the state monad over
    s
    .

The three equality constraints are not exposed in the API, of course.

[edit] 2.3 Operations

Exposed operations of
Ref
,
R
and
M
are the following:
  • The
    Monad
    instance of
    R
    and
    M
  • The monad morphism between
    R
    and
    M
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
.

[edit] 2.3.1 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 ()

[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 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 side-effect, 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).

[edit] 2.4.1 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 over
    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
    MonadTrans
    instance of
    C
    to be able to lift operations in the
    m
    monad.
Note that
C
is parameterized by a monad because in this way it is easier to add other effects later.

[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

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.

[edit] 2.6.2 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 side-effect. 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.

[edit] 2.6.3 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 vice-versa).

Backward lens application can solve long-standing problems with application of lenses, see LGtk/ADT_lenses.

[edit] 2.6.4 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 over
    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
    MonadTrans
    instance of
    C
    to be able to lift operations in the
    m
    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))

[edit] 2.6.5 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 lens-chain are extended. The dependency between the newly created state part and the old state parts can be encoded into the new lens in the lens-chain.

When a previously created reference (i.e. a lens) is accessed with a state after several extensions, a proper prefix of the lens-chain 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, self-adjusting 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 re-adding 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.

[edit] 2.7 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
    and
    M
    are monads,
  • C
    is a monad transformer,
  • liftReadPart :: R a -> M a
    is a monad morphism between
    R
    and
    M
    ,
  • liftMod :: Monad m => M a -> C m a
    is a monad morphism between
    M
    and
    C 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 all
    m :: R a
  • liftM2 (,) m m
    ===
    liftM (\a -> (a, a)) m
    , for all
    m :: 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))

[edit] 3 Effects

TODO