# LGtk/ADT lenses

### From HaskellWiki

m (→Example: List lens) |
(many changes) |
||

Line 57: | Line 57: | ||

The proposed solution, summarized: |
The proposed solution, summarized: |
||

− | '''Use one lens for each ADT type, with reversed direction.''' |
+ | '''As a lens toolbox for an ADT, use a lens whose ''co''domain is the ADT and whose domain is tuple of the constructor tag and the ADT components.''' |

+ | |||

+ | Let's see specific examples before the generic descripton of the proposed lens. |
||

=== Example: List lens === |
=== Example: List lens === |
||

Line 77: | Line 77: | ||

set (l: r) _ = (True, (l, r)) |
set (l: r) _ = (True, (l, r)) |
||

</haskell> |
</haskell> |
||

+ | |||

+ | Here <hask>Bool</hask> is used as the constructor tag, and <hask>a</hask> and <hask>[a]</hask> are the components of the list (head and tail). Intead of a triple we use two pairs, so we reach the parts with <hask>fstLens</hask> and <hask>sndLens</hask>. |
||

=== Usage === |
=== Usage === |
||

Line 86: | Line 88: | ||

</haskell> |
</haskell> |
||

− | If we view the state through <hask>listLens :: Lens S [Int]</hask>, we see a list of <hask>Int</hask>s. So we can view the list. |
||

− | We can edit the list with the following lenses: |
+ | We can view and edit the list through the following lenses: |

+ | |||

+ | * <hask>listLens :: Lens S [Int]</hask> edits the '''complete list'''. |
||

+ | * <hask>fstLens :: Lens S Bool</hask> edits the '''top level constructor''' of the list: <hask>False</hask> corresponds to <hask>[]</hask> and <hask>True</hask> corresponds to <hask>(:)</hask>. |
||

+ | * <hask>headLens = fstLens . sndLens :: Lens S Int</hask> edits the '''head''' of the list. |
||

+ | * <hask>tailLens = sndLens . sndLens :: Lens S [Int]</hask> edits the '''tail''' of the list. |
||

− | * With <hask>fstLens :: Lens S Bool</hask> the top level constructor of the list can be viewed and edited: <hask>False</hask> corresponds to <hask>[]</hask> and <hask>True</hask> corresponds to <hask>(:)</hask>. |
+ | Remarks: |

− | * With <hask>headLens = fstLens . sndLens :: Lens S Int</hask> the first element of the list can be viewed and edited. Note that if the top level constructor of the list is <hask>[]</hask>, the first element can still be edited; the change will only be visible through <hask>listLens</hask> when the constructor is changed back to <hask>(:)</hask>. (This may seem to be odd, but for certain applications this is the right behaviour.) |
||

− | * With <hask>tailLens = sndLens . sndLens :: Lens S Int</hask> the tail of the list can be viewed and edited. |
||

− | Note that for editing the tail of the list, we need an <hask>s' :: S</hask> such that <hask>s</hask> viewed through <hask>tailLens</hask> is the same as <hask>s'</hask> viewed through <hask>listLens</hask>. Explained on a figure: |
+ | * If the top level constructor of the list is <hask>[]</hask>, the head and the tail of the list can still be edited; the change will only be visible through <hask>listLens</hask> when the constructor is changed back to <hask>(:)</hask>. This may seem to be odd, but for many applications this is the right behaviour. |

+ | * For editing the tail of the tail of the list, we need an <hask>s' :: S</hask> such that <hask>s</hask> viewed through <hask>tailLens</hask> is the same as <hask>s'</hask> viewed through <hask>listLens</hask>. Explained on a figure: |
||

[[Image:ADT.png]] |
[[Image:ADT.png]] |
||

− | How <hask>s'</hask> is created is a related but different question. See [[LGtk/Semantics#Dependent_reference_creation]]. |
+ | How <hask>s'</hask> can be created and how <hask>s</hask> and <hask>s'</hask> can be kept in sync is a related but different question. See [[LGtk/Semantics#Dependent_reference_creation]]. |

== Links and references == |
== Links and references == |

## Revision as of 21:48, 7 June 2013

## Contents |

## 1 Problem description

Lenses provide uniform and compositional way to view and edit data structures.

For example, one can view and edit pairs withq == setL fstLens (getL fstLens q) (setL sndLens (getL sndLens q) p)

Similarly, there is a toolbox of lenses for records which toolbox contains one lens for each record field.

Are there a toolbox of lenses for algebraic data types with multiple constructors?

## 2 Existing solutions

### 2.1 Partial lenses

The data-lens library provides partial lenses which are isomorphic to

type PartialLens a b = (a -> Maybe b, a -> Maybe (b -> a))

The flollowing partial lenses are defined for lists:

headLens :: PartialLens [a] a headLens = (get, set) where get [] = Nothing get (h:t) = Just h set [] = Nothing set (h:t) = Just (:t)

tailLens :: PartialLens [a] [a] tailLens = (get, set) where get [] = Nothing get (h:t) = Just t set [] = Nothing set (h:t) = Just (h:)

### 2.2 Other solutions

*Please help to extend the list of known solutions.*

## 3 ADT lenses

The proposed solution, summarized:

**As a lens toolbox for an ADT, use a lens whose codomain is the ADT and whose domain is tuple of the constructor tag and the ADT components.**

Let's see specific examples before the generic descripton of the proposed lens.

### 3.1 Example: List lens

The lens for lists which forms a complete toolbox:

import Data.Lens.Common

listLens :: Lens (Bool, (a, [a])) [a] listLens = lens get set where get (False, _) = [] get (True, (l, r)) = l: r set [] (_, x) = (False, x) set (l: r) _ = (True, (l, r))

### 3.2 Usage

Suppose that we have a statetype S = (Bool, (Int, [Int]))

We can view and edit the list through the following lenses:

- edits thelistLens :: Lens S [Int]
**complete list**. - edits thefstLens :: Lens S Bool
**top level constructor**of the list:corresponds toFalseand[]corresponds toTrue.(:) - edits theheadLens = fstLens . sndLens :: Lens S Int
**head**of the list. - edits thetailLens = sndLens . sndLens :: Lens S [Int]
**tail**of the list.

Remarks:

- If the top level constructor of the list is , the head and the tail of the list can still be edited; the change will only be visible through[]when the constructor is changed back tolistLens. This may seem to be odd, but for many applications this is the right behaviour.(:)
- For editing the tail of the tail of the list, we need an such thats' :: Sviewed throughsis the same astailLensviewed throughs'. Explained on a figure:listLens

## 4 Links and references

I have not seen this technique described before. Please help to extend the list of papers / blog entries, where this or similar technique is used.

[Reddit comments]