# LGtk/ADT lenses

### From HaskellWiki

(begin to document ADT lenses) |
(remark: put-put does not hold) |
||

(24 intermediate revisions by one user not shown) | |||

Line 3: | Line 3: | ||

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

− | For example, one can view and edit pairs with <hask>fstLens</hask> and <hask>sndLens</hask>. <hask>fstLens</hask> and <hask>sndLens</hask> forms a complete toolbox for editing pairs in the sense that given pairs <hask>p :: (a, b)</hask> and <hask>q :: (a, b)</hask>, with succesive get and set operations <hask>p</hask> can be changed to be equivalent to <hask>q</hask>: <hask>setL fstLens (getL fstLens q) $ setL sndLens (getL sndLens q) p</hask>. |
+ | For example, one can view and edit pairs with <hask>fstLens</hask> and <hask>sndLens</hask>. These two lenses form a toolbox for editing pairs in the sense that given pairs <hask>p :: (a, b)</hask> and <hask>q :: (a, b)</hask>, by succesive get and set operations <hask>p</hask> can be changed to be equivalent to <hask>q</hask>: |

− | Similarly, there is a complete toolbox of lenses for records, the toolbox contains one lens for each record field. |
+ | <haskell> |

+ | q == setL fstLens (getL fstLens q) (setL sndLens (getL sndLens q) p) |
||

+ | </haskell> |
||

+ | |||

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

+ | |||

+ | '''Question:''' |
||

− | Now, the problem is, are there a toolbox of lenses for algebraic data types with multiple constructors? |
+ | Is there a toolbox of lenses for an algebraic data type with multiple constructors? |

== Existing solutions == |
== Existing solutions == |
||

Line 16: | Line 16: | ||

<haskell> |
<haskell> |
||

− | type PartialLens a b = (a -> Maybe b, a -> Maybe (b -> a)) |
+ | type PartialLens a b = a -> Maybe (b, b -> a) |

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

− | The flollowing partial lenses are defined for lists: |
+ | The following partial lenses are defined for lists: |

<haskell> |
<haskell> |
||

headLens :: PartialLens [a] a |
headLens :: PartialLens [a] a |
||

− | headLens = (get, set) |
+ | headLens [] = Nothing |

− | where |
+ | headLens (h:t) = Just (h, (:t)) |

− | get [] = Nothing |
||

− | get (h:t) = Just h |
||

− | |||

− | set [] = Nothing |
||

− | set (h:t) = Just (:t) |
||

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

<haskell> |
<haskell> |
||

tailLens :: PartialLens [a] [a] |
tailLens :: PartialLens [a] [a] |
||

− | tailLens = (get, set) |
+ | tailLens [] = Nothing |

− | where |
+ | tailLens (h:t) = Just (t, (h:)) |

− | get [] = Nothing |
||

− | get (h:t) = Just t |
||

− | |||

− | set [] = Nothing |
||

− | set (h:t) = Just (h:) |
||

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

Line 37: | Line 37: | ||

=== Other solutions === |
=== Other solutions === |
||

− | Please help to extend the list of known solutions. |
+ | ''Please help to extend the list of known solutions.'' |

== ADT lenses == |
== ADT lenses == |
||

Line 43: | Line 43: | ||

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 a tuple of the constructor tag and the ADT components.''' |

+ | |||

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

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

− | The ADT lens for lists: |
+ | The lens for lists which forms a complete toolbox: |

<haskell> |
<haskell> |
||

Line 64: | Line 64: | ||

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

− | === Usage === |
+ | 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>. |

+ | |||

+ | ==== List lens usage ==== |
||

Suppose that we have a state <hask>s</hask> of type |
Suppose that we have a state <hask>s</hask> of type |
||

Line 72: | Line 72: | ||

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

− | * 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>. |
+ | * <hask>listLens :: Lens S [Int]</hask> edits the '''complete list'''. |

− | * 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.) |
+ | * <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>. |

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

− | Note that for editing the tail of the list, we need <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: |
+ | Remarks: |

+ | |||

+ | * 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. See the interpretation subsection below. |
||

+ | * 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]] |
||

+ | |||

+ | On the figure, edges are lenses and nodes are ''references''. One possible definition of references is given in [[LGtk/Semantics#References]]. How <hask>s'</hask> can be created and how <hask>s</hask> and <hask>s'</hask> can be kept in sync is an important but separate question. [[LGtk/Semantics#Dependent_reference_creation]] describes a possible solution. |
||

+ | |||

+ | === Example: ADT with repeated record fields === |
||

+ | |||

+ | Consider the following ADT: |
||

+ | |||

+ | <haskell> |
||

+ | data X a |
||

+ | = X1 { y :: Int, z :: a } |
||

+ | | X2 { y :: Int, v :: Char } |
||

+ | </haskell> |
||

+ | |||

+ | Note that the <hask>y</hask> field is defined twice. |
||

+ | |||

+ | For the ADT lens, first define an auxiliary enum type for the constructor tags: |
||

+ | |||

+ | <haskell> |
||

+ | data XTag = X1Tag | X2Tag |
||

+ | </haskell> |
||

+ | |||

+ | The definition of <hask>XTag</hask> is kind of inevitable if we would like to edit the constructor tags. We could use <hask>Bool</hask>, but that would not scale to more constructors. We could use <hask>Int</hask> too, but with less static checks from the type system. |
||

+ | |||

+ | The definition of the lens toolbox for <hask>X</hask>: |
||

+ | |||

+ | <haskell> |
||

+ | xLens :: Lens (XTag, (Int, (a, Char))) (X a) |
||

+ | xLens = lens get set where |
||

+ | |||

+ | get (X1Tag, (y, (z, _))) = X1 y z |
||

+ | get (X2Tag, (y, (_, v))) = X2 y v |
||

+ | |||

+ | set (X1 y z) (_, (_, (_, v))) = (X1Tag, (y, (z, v))) |
||

+ | set (X2 y v) (_, (_, (z, _))) = (X2Tag, (y, (z, v))) |
||

+ | </haskell> |
||

+ | |||

+ | Remarks: |
||

+ | |||

+ | * Instead of <hask>(XTag, (Int, (a, Char)))</hask>, we could use <hask>(XTag, (Int, a, Char))</hask> or <hask>(XTag, Int, a, Char)</hask> too. This is an implementation detail. |
||

+ | * <hask>xLens</hask> remembers the value of <hask>y</hask> if we change between the constructor tags. This is the intended behaviour. |
||

+ | * <hask>xLens</hask> remembers the values of <hask>v</hask> and <hask>z</hask> fields if we change between the constructor tags. This is the intended behaviour. |
||

+ | |||

+ | ==== Interpreation ==== |
||

+ | |||

+ | The intended behaviour can be justified if we interpret lenses as abstract editors. If we would like to define an editor of an <hask>X</hask> value, the state of the editor would be <hask>(XTag, (Int, (a, Char)))</hask>, and one could retrive the actual <hask>X</hask> value by <hask>xLens</hask> from the state. The editor would be the composition of the following simpler editors: |
||

+ | |||

+ | * An elementary editor for <hask>XTag</hask> (maybe a combo box or a checkbox) which would be connected to the editor state by <hask>fstLens</hask>. |
||

+ | * An elementary editor for an <hask>Int</hask> (maybe a text box or a slider) which would be connected to the editor state by <hask>fstLens . sndLens</hask>. |
||

+ | * An editor for an <hask>a</hask> typed value which would be connected to the editor state by <hask>fstLens . sndLens . sndLens</hask>. |
||

+ | * An editor for a <hask>Char</hask> (maybe a combo box or a text box or a virtual keyboard) which would be connected to the editor state by <hask>sndLens . sndLens . sndLens</hask>. |
||

+ | |||

+ | Now, the intended behaviour is the following: |
||

+ | |||

+ | * If the user fills in an <hask>Int</hask> value for <hask>y</hask>, this value should remain the same after changing the <hask>XTag</hask> value. |
||

+ | * The <hask>a</hask> value editor should be active only if the <hask>XTag</hask> value is <hask>X1Tag</hask>. |
||

+ | * The <hask>Char</hask> editor should be active only if the <hask>XTag</hask> value is <hask>X2Tag</hask>. |
||

+ | * If the user fills in an <hask>a</hask> value for <hask>z</hask> when the <hask>XTag</hask> value is <hask>X1Tag</hask>, and the user changes <hask>X1Tag</hask> to <hask>X2Tag</hask> and then back to <hask>X1Tag</hask>, the <hask>a</hask> value should be the same as before (consider a complex value which is hard to re-create). Similar holds for the <hask>Char</hask> value. |
||

+ | |||

+ | === Generic ADT lens === |
||

+ | |||

+ | In the generic case, consider the following ADT: |
||

+ | |||

+ | <haskell> |
||

+ | data X a1 ... aN |
||

+ | = X1 { x11 :: t11, x12 :: t12, ... } |
||

+ | | X2 { x21 :: t21, x22 :: t22, ... } |
||

+ | ... |
||

+ | | XM { xM1 :: tM1, xM2 :: tM2, ... } |
||

+ | </haskell> |
||

+ | |||

+ | Suppose that the set of different field names is <hask>f1 :: s1</hask>, <hask>f2 :: s2</hask>, ..., <hask>fK :: sK</hask>. |
||

+ | |||

+ | Let <hask>cij</hask> be equal to <hask>k</hask> iff <hask>xij</hask> is equal to <hask>fk</hask>. |
||

+ | |||

+ | Define an auxiliary enum type for the constructor tags: |
||

+ | |||

+ | <haskell> |
||

+ | data XTag = X1Tag | X2Tag | ... | XMTag |
||

+ | </haskell> |
||

+ | |||

+ | The definition of the lens toolbox for <hask>X</hask>: |
||

+ | |||

+ | <haskell> |
||

+ | xLens :: Lens (XTag, (s1, (s2, ...))) (X a1 ... aN) |
||

+ | xLens = lens get set where |
||

+ | |||

+ | get (X1Tag, (s1, (s2, ...))) = X1 s{c11} s{c12} ... |
||

+ | ... |
||

+ | get (XMTag, (s1, (s2, ...))) = X2 s{cM1} s{cM2} ... |
||

+ | |||

+ | -- replace second occurrence of the same variable name by _ in pattern |
||

+ | set (X1 s{c11} s{c12} ...) (_, (s1, (s2, ...))) = (X1Tag, (s1, (s2, ...))) |
||

+ | ... |
||

+ | set (XM s{cM1} s{cM2} ...) (_, (s1, (s2, ...))) = (XMTag, (s1, (s2, ...))) |
||

+ | </haskell> |
||

+ | |||

+ | == Lens laws == |
||

+ | |||

+ | The ADT lenses defined above are not very well-behaved lenses, the put-put law does not hold. For example, |
||

+ | |||

+ | <haskell> |
||

+ | setL listLens [] (setL listLens ['a'] (False, ('b', []))) == (False, ('a', [])) |
||

+ | </haskell> |
||

+ | |||

+ | <haskell> |
||

+ | setL listLens [] (False, ('b', []))) == (False, ('b', [])) |
||

+ | </haskell> |
||

+ | == Summary == |
||

+ | With the proposed ADT lenses, one can do arbitrary edit actions on ADT values in a user-friendly way (both distinct and common ADT parts are remembered when switching between constructors). |
||

+ | Note however, that the put-put law does not holds for the proposed ADT lenses. |
||

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

Line 90: | Line 92: | ||

Please help to extend the list of papers / blog entries, where this or similar technique is used. |
Please help to extend the list of papers / blog entries, where this or similar technique is used. |
||

− | [Reddit comments] |
+ | [http://www.reddit.com/r/haskell/comments/1fw7pm/adt_lenses/ Reddit comments] |

## Latest revision as of 18:10, 8 June 2013

## Contents |

## [edit] 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.

**Question:**

Is there a toolbox of lenses for an algebraic data type with multiple constructors?

## [edit] 2 Existing solutions

### [edit] 2.1 Partial lenses

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

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

The following partial lenses are defined for lists:

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

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

### [edit] 2.2 Other solutions

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

## [edit] 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 a tuple of the constructor tag and the ADT components.**

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

### [edit] 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))

#### [edit] 3.1.1 List lens 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. See the interpretation subsection below.(:)
- 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

*references*. One possible definition of references is given in LGtk/Semantics#References. How

### [edit] 3.2 Example: ADT with repeated record fields

Consider the following ADT:

data X a = X1 { y :: Int, z :: a } | X2 { y :: Int, v :: Char }

For the ADT lens, first define an auxiliary enum type for the constructor tags:

data XTag = X1Tag | X2Tag

xLens :: Lens (XTag, (Int, (a, Char))) (X a) xLens = lens get set where get (X1Tag, (y, (z, _))) = X1 y z get (X2Tag, (y, (_, v))) = X2 y v set (X1 y z) (_, (_, (_, v))) = (X1Tag, (y, (z, v))) set (X2 y v) (_, (_, (z, _))) = (X2Tag, (y, (z, v)))

Remarks:

- Instead of , we could use(XTag, (Int, (a, Char)))or(XTag, (Int, a, Char))too. This is an implementation detail.(XTag, Int, a, Char)
- remembers the value ofxLensif we change between the constructor tags. This is the intended behaviour.y
- remembers the values ofxLensandvfields if we change between the constructor tags. This is the intended behaviour.z

#### [edit] 3.2.1 Interpreation

The intended behaviour can be justified if we interpret lenses as abstract editors. If we would like to define an editor of an- An elementary editor for (maybe a combo box or a checkbox) which would be connected to the editor state byXTag.fstLens
- An elementary editor for an (maybe a text box or a slider) which would be connected to the editor state byInt.fstLens . sndLens
- An editor for an typed value which would be connected to the editor state bya.fstLens . sndLens . sndLens
- An editor for a (maybe a combo box or a text box or a virtual keyboard) which would be connected to the editor state byChar.sndLens . sndLens . sndLens

Now, the intended behaviour is the following:

- If the user fills in an value forInt, this value should remain the same after changing theyvalue.XTag
- The value editor should be active only if theavalue isXTag.X1Tag
- The editor should be active only if theCharvalue isXTag.X2Tag
- If the user fills in an value forawhen thezvalue isXTag, and the user changesX1TagtoX1Tagand then back toX2Tag, theX1Tagvalue should be the same as before (consider a complex value which is hard to re-create). Similar holds for theavalue.Char

### [edit] 3.3 Generic ADT lens

In the generic case, consider the following ADT:

data X a1 ... aN = X1 { x11 :: t11, x12 :: t12, ... } | X2 { x21 :: t21, x22 :: t22, ... } ... | XM { xM1 :: tM1, xM2 :: tM2, ... }

Define an auxiliary enum type for the constructor tags:

data XTag = X1Tag | X2Tag | ... | XMTag

xLens :: Lens (XTag, (s1, (s2, ...))) (X a1 ... aN) xLens = lens get set where get (X1Tag, (s1, (s2, ...))) = X1 s{c11} s{c12} ... ... get (XMTag, (s1, (s2, ...))) = X2 s{cM1} s{cM2} ... -- replace second occurrence of the same variable name by _ in pattern set (X1 s{c11} s{c12} ...) (_, (s1, (s2, ...))) = (X1Tag, (s1, (s2, ...))) ... set (XM s{cM1} s{cM2} ...) (_, (s1, (s2, ...))) = (XMTag, (s1, (s2, ...)))

## [edit] 4 Lens laws

The ADT lenses defined above are not very well-behaved lenses, the put-put law does not hold. For example,

setL listLens [] (setL listLens ['a'] (False, ('b', []))) == (False, ('a', []))

setL listLens [] (False, ('b', []))) == (False, ('b', []))

## [edit] 5 Summary

With the proposed ADT lenses, one can do arbitrary edit actions on ADT values in a user-friendly way (both distinct and common ADT parts are remembered when switching between constructors).

Note however, that the put-put law does not holds for the proposed ADT lenses.

## [edit] 6 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.