View source for LGtk/Semantics

The semantics of LGtk is given by a reference implementation.
The reference implementation is given in the following stages.

= Lenses =

LGtk use simple lenses defined in the data-lens package:

<haskell>
newtype Lens a b = Lens { runLens :: a -> Store b a }
</haskell>

This data type is isomorphic to <hask>(a -> b, b -> a -> a)</hask>, the well-know lens data type. The isomorphism is established by the following operations:

<haskell>
getL :: Lens a b -> a -> b
</haskell>

<haskell>
setL :: Lens a b -> b -> a -> a
</haskell>

<haskell>
lens :: (a -> b) -> (b -> a -> a) -> Lens a b
</haskell>

== Lens laws ==

The three well-known laws for lenses:

* get-set: <hask>set k (get k a) a</hask> === <hask>a</hask>
* set-get: <hask>get k (set k b a)</hask> === <hask>b</hask>
* set-set: <hask>set k b2 (set k b1 a)</hask> === <hask>set k b2 a</hask>

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

= References =

It is convenient to use lenses with the state monad
([http://www.haskellforall.com/2013/05/program-imperatively-using-haskell.html see this use case]) and the reader monad.

Let's call a value with type <hask>Lens s a</hask> a '''reference''' of the state monad <hask>State s</hask> and the reader monad <hask>Reader s</hask>.

References are distinguished from lenses, because we would like to make the program state <hask>s</hask> unaccessible to guarantee linear use of the state for example.

There are several ways to model references in Haskell.
LGtk models them as type classes with associated types, but that is just a technical detail.

== Types ==

Instead of giving a concrete implementation in Haskell, suppose that

* <hask>s</hask> is a fixed type,
* <hask>Ref :: * -> *</hask> ~ <hask>Lens s</hask>, references are lenses from <hask>s</hask> to the type of the referred value,
* <hask>R :: * -> *</hask> ~ <hask>Reader s</hask>, the '''reference reading monad''' is the reader monad over <hask>s</hask>,
* <hask>S :: * -> *</hask> ~ <hask>State s</hask>, the '''reference reading and writing monad''' is the state monad over <hask>s</hask>.

The three equality constraints are not exposed in the API.

== Operations ==

Exposed operations of <hask>Ref</hask>, <hask>S</hask> and <hask>R</hask>:

* The <hask>Monad</hask> instance of <hask>S</hask> and <hask>R</hask>

* The monad morphism between <hask>R</hask> and <hask>S</hask>

<haskell>
liftReadPart :: R a -> S a
liftReadPart = gets . runReader
</haskell>

* Reference read

<haskell>
readRef :: Ref a -> R a
readRef = reader . getL
</haskell>

* Reference write

<haskell>
writeRef :: Ref a -> a -> S ()
writeRef = modify . setL r
</haskell>

* Lens application on a reference

<haskell>
lensMap :: Lens a b -> Ref a -> Ref b
lensMap = (.)
</haskell>

* Reference join

<haskell>
joinRef :: R (Ref a) -> Ref a
joinRef = Lens . join . (runLens .) . runReader 
</haskell>

* The unit reference

<haskell>
unitRef :: Ref ()
unitRef = lens (const ()) (const id) 
</haskell>

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

== Reference creation ==

There should be a possibility for new reference creation too.

New reference creation with a given initial value extends the state. For example, if the state is <hask>(1, 'c') :: (Int, Char)</hask>, extending the state with <hask>True :: Bool</hask> would yield the state <hask>((1, 'c'), True) :: ((Int, Char), Bool)</hask>.

We could model the type change of the state with an [http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Monad-Indexed.html 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''', a data type <hask>S</hask> with the operations

<haskell>
empty :: S
</haskell>

<haskell>
extend :: a -> State S (Lens S a)
</haskell>

such that the following laws hold:

* <hask>extend v >> return ()</hask> === <hask>return ()</hask>

* <hask>extend v >>= liftReadPart . readRef</hask> === <hask>return v</hask>

The first law sais that <hask>extend</hask> 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 <hask>v</hask> creates a reference with inital value <hask>v</hask>.

Is there a state with a well-behaved extend function?

The answer is '''yes''', but we should guarantee linear usage of the state. This is great, because linear usage is guaranteed with the restricted API!

How can such an <hask>S</hask> be implemented? And how can such an <hask>S</hask> be implemented efficiently? These questions are not relevant for the semantics, but there is an efficient implementation with <hask>IORef</hask>s.

== Reference creation API ==

Let <hask>S</hask> be an extensible state as specified before.
Let <hask>s</hask> = <hask>S</hask> in the definition of references.

* <hask>C :: (* -> *) -> * -> *</hask> ~ <hask>StateT S</hask>, the '''reference creating monad''' is the state monad transformer over <hask>S</hask>.

The equality constraint is not exposed in the API.
The following functions are exposed:

* New reference creation

<haskell>
newRef :: Monad m => a -> C m (Ref a)
newRef v = mapStateT (return . runIdentity) $ extend v
</haskell>

* Lift reference read and write operations

<haskell>
liftWrite :: Monad m => S a -> C m a
liftWrite = mapStateT (return . runIdentity)
</haskell>

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

Note that <hask>C</hask> is parameterized by a monad because in this way it is easier to add other effects later.

== Running ==

The last missing function in the API is the running of the <hask>C m</hask> monad.

* Run the reference creation monad

<haskell>
runC :: Monad m => C m a -> m a
runC x = runStateT x empty
</haskell>

= Lens-trees =

TODO

= Effects =

TODO