Editing LGtk/ADT lenses (section)

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