# LGtk/Semantics

### From HaskellWiki

m (→Reference creation) |
m (→Reference creation) |
||

Line 143: | Line 143: | ||

The answer is '''yes''', but we should guarantee linear usage of the state. The (constructive) existence proof is given in the next section. |
The answer is '''yes''', but we should guarantee linear usage of the state. The (constructive) existence proof is given in the next section. |
||

− | The linear usage of state is guaranteed with refereces API (check the definitions), which means that we have a solution. |
+ | 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? However this question is not relevant for the semantics, we will see that there is an efficient implementation with <hask>MVar</hask>s. |
+ | 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 <hask>MVar</hask>s (TODO). |

=== Reference creation API === |
=== Reference creation API === |

## Revision as of 20:15, 2 June 2013

The semantics of LGtk is given by a reference implementation. The reference implementation is given in three stages: lenses, references and effects.

## Contents |

## 1 Lenses

LGtk uses simple lenses defined in the data-lens 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

### 1.1 Lens laws

The three well-known laws for lenses:

- get-set: ===set k (get k a) aa
- set-get: ===get k (set k b a)b
- set-set: ===set k b2 (set k b1 a)set k b2 a

Impure lenses, i.e. lenses which brake lens laws are allowed in certain places. Those places are explicitly marked and explained in this overview.

## 2 References

### 2.1 Motivation

LetWe have the following goals:

- Define a structure similar to in which(Lens s, State s, Reader s)is not accessable.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.

### 2.2 Types

We keep the typesInstead of giving a concrete implementation in Haskell, suppose that

- is a fixed arbitrary type,s
- ~Ref :: * -> *;Lens s
**references**are lenses fromto the type of the referred value,s - ~R :: * -> *; theReader s
**reference reading monad**is the reader monad over,s - ~M :: * -> *; theState s
**reference modifying monad**is the state monad over.s

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

### 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)

**not**a reference because that would leak the program state

### 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 type

`empty :: 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### 2.5 Reference creation API

Let- ~C :: (* -> *) -> * -> *, theStateT S
**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 v = mapStateT (return . runIdentity) $ extend v

- 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

### 2.6 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

### 2.7 Lens-stacks

#### 2.7.1 Motivation

We can extend the state in an independent way (the new state piece is independent from the others). This may not be enough for modular design.

Suppose that we have a referenceThe problem is that we cannot remember the value of the entry field if the checkbox is unchecked! Lens-stacks give a nice solution to this problem.

#### 2.7.2 Low-level API

Let's begin with the API. Suppose that we have an abstract data type`empty :: S`

extend' :: Lens S b -> Lens a b -> a -> State S (Lens S a)

such that the following laws hold:

- Law 1: has no side-effect:extend'

- Law 2: applied on the result ofkbehaves asextend' r k a0:r

- Law 3: Initialization of the newly defined reference:

#### 2.7.3 Usage

Law 2 is the most interesting, it sais that we can**apply a lens backwards**with

**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)

Backward lens application can solve several long-standing problems with lenses, but it is another story to show that.

#### 2.7.4 References API

Let- ~C :: (* -> *) -> * -> *, theStateT S
**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 a0 = mapStateT (return . runIdentity) $ extend' r k a0

- 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))

#### 2.7.5 Implementation

We prove constructively, by giving a reference implementation, thatReference implementation:

Let**lens-chains**, 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

Auxiliary functions:

chainToLens :: Chain a b -> Lens a b chainToLens = ...

type S = forall a . S { value :: a , chain :: Chain a () }

empty :: S empty = S () []

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 r12 = setL r2 . getL r1 f x0@(S value0 chain0) = ( k' . chainToLens (take (length chain - length chain0) chain) , S (r12 x0 a0, value0) (k : chain0) ) where k = lens snd $ \x (a, _) -> (r12 x a, x) k' = lens fst $ \a (_, x) -> (a, r21 a x)

TODO: more explanation of the code

## 3 Effects

TODO