LGtk/Semantics

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

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

Lens laws

The three well-known laws for lenses:

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

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.

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.

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 MVars (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 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

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

Lens-chains

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! Lens-chains give a nice solution to this problem.

Low-level API

Let's begin with the API. Suppose that we have an abstract data type S with the following 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.

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 several long-standing problems with application of lenses, but it is another story to show that.

References 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:

• 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 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 expressive than newRef:

newRef :: Monad m => a -> C m (Ref a)
newRef = extRef unitRef (lens (const ()) (const id))

Implementation

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

When a new reference is created, both the state and the lens-chain 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 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 new state such that it fits the previously created reference.

Reference implementation:

Let Chain a b be the type of 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 a and the codomain of the last lens is b.

Suppose that we have the following auxiliary functions:

chainToLens :: Chain a b -> Lens a b

emptyChain :: Chain a a

chainCons :: Lens a b -> Chain b c -> Chain a c

chainLength :: Chain a b -> Int

The definition of S (an existentional type):

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

Definition of empty:

empty :: S
empty = S () emptyChain

Definition of extend':

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 (takeChain (length chain - length chain0) chain)
          , S (r12 x0 a0, value0) (chainCons k chain0)
          )
      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 ?

The code does not compile because takeChain is not defined. takeChain cannot be given a proper type in this context. However, if we suppose that values of S are used linearly, types will match at runtime with the naive implementation of takeChain. This means that unsafeCoerce can be used safely to force the Haskell compiler to accept the code.

Effects

TODO