View source for LGtk/ADT lenses

== Problem description ==

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

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

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

== Existing solutions ==

=== Partial lenses ===

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

<haskell>
type PartialLens a b = a -> Maybe (b, b -> a)
</haskell>

The following partial lenses are defined for lists:

<haskell>
headLens :: PartialLens [a] a
headLens [] = Nothing
headLens (h:t) = Just (h, (:t))
</haskell>

<haskell>
tailLens :: PartialLens [a] [a]
tailLens [] = Nothing
tailLens (h:t) = Just (t, (h:))
</haskell>

Unfortunately <hask>headLens</hask> and <hask>tailLens</hask> does not provide a complete toolbox, one cannot change an empty list to a non-empty list with them, for example.

=== Other solutions ===

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

== ADT lenses ==

The proposed solution, summarized:

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

The lens for lists which forms a complete toolbox:

<haskell>
import Data.Lens.Common
</haskell>

<haskell>
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))
</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>.

==== List lens usage ====

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

<haskell>
type S = (Bool, (Int, [Int]))
</haskell>


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.

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

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.

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