Safe Haskell | Trustworthy |
---|---|

Language | Haskell2010 |

This module provides an "applicative" (functional) way of composing
lenses through the data type `L`

. For example, this module enables us
to define a "lens" version of `unlines`

as follows.

unlinesF :: [L s String] -> L s String unlinesF [] = new "" unlinesF (x:xs) = catLineF x (unlinesF xs) where catLineF = lift2 catLineL catLineL :: Lens' (String, String) String catLineL = ...

To make a lens from such "lens functions", one can use unlifting
functions (`unlift`

, `unlift2`

, `unliftT`

) as follows.

unlinesL :: Lens' [String] String unlinesL = unliftT unlinesF

The obtained lens works as expected (here `^.`

, `&`

and `.~`

are taken from Control.Lens).

`>>>`

"banana\norange\napple\n"`["banana", "orange", "apple"] ^. unlinesL`

`>>>`

["Banana","Orange","Apple"]`["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple\n"`

One can understand that `L s a`

is an updatable `a`

.
The type `[L s String] -> L s String`

of `unlinesF`

tells us that
we can update only the list elements.
Actually, insertion or deletion of lines to the view will fail, as below.

`>>>`

*** Exception: ...`["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple"`

`>>>`

*** Exception: ...`["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple\n\n"`

If you want to reflect insertions and deletions, one have to write a
function of type `L s [String] -> L s String`

, which says that the
list structure itself would be updatable. To write a function of this
type, `liftC`

and `liftC2`

functions would be sometimes useful.

unlinesF' :: L s [String] -> L s String unlinesF' = liftC (foldWithDefault "" "n") (lift catLineL') catLineL' :: Lens' (Either () (String,String)) String catLineL' = ... foldWithDefault :: a -> (Lens' (Either () (a,b)) b) -> Lens' [a] b foldWithDefault d f = ...

- data L s a
- lens' :: (s -> (v, v -> s)) -> Lens' s v
- unit :: L s ()
- pair :: L s a -> L s b -> L s (a, b)
- list :: [L s a] -> L s [a]
- sequenceL :: (Eq (t ()), Traversable t) => t (L s a) -> L s (t a)
- new :: Eq a => a -> L s a
- lift :: Lens' a b -> forall s. L s a -> L s b
- lift2 :: Lens' (a, b) c -> L s a -> L s b -> L s c
- liftT :: (Eq (t ()), Traversable t) => Lens' (t a) b -> forall s. t (L s a) -> L s b
- liftLens :: (a -> b) -> (a -> b -> a) -> forall s. L s a -> L s b
- liftLens' :: (a -> (b, b -> a)) -> forall s. L s a -> L s b
- unlift :: Eq a => (forall s. L s a -> L s b) -> Lens' a b
- unlift2 :: (Eq a, Eq b) => (forall s. L s a -> L s b -> L s c) -> Lens' (a, b) c
- unliftT :: (Eq a, Eq (t ()), Traversable t) => (forall s. t (L s a) -> L s b) -> Lens' (t a) b
- data R s a
- observe :: Eq w => L s w -> R s w
- liftO :: Eq w => (a -> w) -> L s a -> R s w
- liftO2 :: Eq w => (a -> b -> w) -> L s a -> L s b -> R s w
- unliftM :: Eq a => (forall s. L s a -> R s (L s b)) -> Lens' a b
- unliftM2 :: (Eq a, Eq b) => (forall s. L s a -> L s b -> R s (L s c)) -> Lens' (a, b) c
- unliftMT :: (Eq a, Eq (t ()), Traversable t) => (forall s. t (L s a) -> R s (L s b)) -> Lens' (t a) b
- liftC :: Eq a => (Lens' a b -> Lens' c d) -> (forall s. L s a -> L s b) -> forall s. L s c -> L s d
- liftC2 :: (Eq a, Eq c) => (Lens' a b -> Lens' c d -> Lens' e f) -> (forall s. L s a -> L s b) -> (forall s. L s c -> L s d) -> forall s. L s e -> L s f
- module Control.LensFunction.Exception

# Core Datatype

An abstract type for "updatable" data. Bidirectional programming through our module is to write manipulation of this datatype.

#### Categorical Notes

The type constructor `L s`

together with `lift`

, `unit`

and `pair`

defines a lax monoidal functor from the category of lenses to that of
Haskell functions. The `lift`

function does transfor a lens to a
function. The `unit`

and `pair`

functions are the core operations on
this lax monoidal functor. Any lifting functions defined in this
module can be defined by these three functions.

# Other constructors for `Lens'`

lens' :: (s -> (v, v -> s)) -> Lens' s v Source #

A variant of `lens`

. Sometimes, this function would be
easier to use because one can re-use a source information to define a "put".

# Functions handling pairs and containers

The unit element in the lifted world.

Let `elimUnitL`

and `elimUnitR`

are lenses defined as follows.

elimUnitL = lens ((x,()) -> x) (_ x -> (x,())) elimUnitR = lens (((),x) -> x) (_ x -> ((),x))

Then, we have the following laws.

lift2 elimUnitL x unit = x

lift2 elimUnitR unit x = x

pair :: L s a -> L s b -> L s (a, b) Source #

A paring function of `L s a`

-typed values.
This function can be defined by `lift2`

as below.

pair = lift2 (lens id (const id))

sequenceL :: (Eq (t ()), Traversable t) => t (L s a) -> L s (t a) Source #

A data-type generic version of `list`

. The contraint `Eq (t ())`

says that we can check the equivalence of shapes of containers `t`

.

# Lifting Functions

new :: Eq a => a -> L s a Source #

The nullary version of a lifting function. Since there is no source,
every view generated by `new`

is not updatable.

The function will throw `ConstantUpdateException`

, if its view is
updated.

lift :: Lens' a b -> forall s. L s a -> L s b Source #

The lifting function. Note that it forms a functor from the category of lenses to the category of sets and functions.

`unlift`

is a left-inverse of this function.

unlift (lift x) = x

lift2 :: Lens' (a, b) c -> L s a -> L s b -> L s c Source #

The lifting function for binary lenses. `unlift2`

is a left inverse of this function.

unlift2 (lift2 l) = l

This function can be defined from `lift`

and `pair`

as below.

lift2 l x y = lift l (pair x y)

NB: This is not a right inverse of `unlift2`

.

(\x y -> x) /= lift2 (unlift2 (\x y -> x))

`>>>`

"B"`set (unlift (\z -> (\x y -> x) z z)) "A" "B"`

`>>>`

Error: ...`set (unlift (\z -> lift2 (unlift2 (\x y -> x)) (z,z))) "A" "B"`

liftT :: (Eq (t ()), Traversable t) => Lens' (t a) b -> forall s. t (L s a) -> L s b Source #

A datatype-generic version of `lift2`

liftLens :: (a -> b) -> (a -> b -> a) -> forall s. L s a -> L s b Source #

Just a composition of `lift`

and `lens`

.
Sometimes, this function would be more efficient than the composition
due to eliminated conversion from the lens to the internal representation.

Since both of the internal and the external representations are functions (= normal forms), we have to pay the conversion cost for each time when the lifted lens function is evaluated, even in the lazy evaluation.

We actually has the RULE to make the composition of `lift`

and
`lens`

to `liftLens`

. However, the rule may not be fired
especially when profiling codes are inserted by GHC.

# Unlifting Functions

unlift :: Eq a => (forall s. L s a -> L s b) -> Lens' a b Source #

The unlifting function, satisfying `unlift (lift x) = x`

.

unlift2 :: (Eq a, Eq b) => (forall s. L s a -> L s b -> L s c) -> Lens' (a, b) c Source #

The unlifting function for binary functions, satisfying
`unlift2 (lift2 x) = x`

.

unliftT :: (Eq a, Eq (t ()), Traversable t) => (forall s. t (L s a) -> L s b) -> Lens' (t a) b Source #

The unlifting function for functions that manipulate data structures,
satisfying `unliftT (liftT x) = x`

if `x`

keeps the shape.
The constraint `Eq (t ())`

says that we can compare the shapes of
given two containers.

# Functions for Handling Observations

## Core Monad

An abstract monad used to keep track of observations. By this monad, we can inspect the value of 'L s a'-data.

It is worth noting that we cannot change the inspection result to ensure the consistency property (aka PutGet in some context).

## Lifting Observations

observe :: Eq w => L s w -> R s w Source #

A primitive used to define `liftO`

and `liftO2`

.
With `observe`

, one can inspect the current value of a lifted '(L s a)'-value
as below.

```
f x :: L s A -> R s (L s B)
f x = do viewX <- observe x
... computation depending on
````viewX`

...

Once the `observe`

function is used in a lens function,
the lens function becomes not able to change
change the "observed" value to ensure the correctness.

liftO :: Eq w => (a -> w) -> L s a -> R s w Source #

Lifting of observations. A typical use of this function would be as follows.

f x :: L s Int -> R s (L s B) f x = do b liftO ( 0) x if b then ... else ...

## Unlifting Functions

unliftM :: Eq a => (forall s. L s a -> R s (L s b)) -> Lens' a b Source #

A monadic version of `unlift`

.

unliftM2 :: (Eq a, Eq b) => (forall s. L s a -> L s b -> R s (L s c)) -> Lens' (a, b) c Source #

A monadic version of `unlift2`

.

unliftMT :: (Eq a, Eq (t ()), Traversable t) => (forall s. t (L s a) -> R s (L s b)) -> Lens' (t a) b Source #

A monadic version of `unliftT`

.

# Lifting Functions for Combinators

liftC :: Eq a => (Lens' a b -> Lens' c d) -> (forall s. L s a -> L s b) -> forall s. L s c -> L s d Source #

A lifting function for lens combinators. One can understand that the universal quantification for the second argument as closedness restriction.