Personal tools

LGtk/ADT lenses

From HaskellWiki

< LGtk(Difference between revisions)
Jump to: navigation, search
(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 with
fstLens
and
sndLens
. These two lenses form a toolbox for editing pairs in the sense that given pairs
p :: (a, b)
and
q :: (a, b)
, by succesive get and set operations
p
can be changed to be equivalent to
q
:
q == 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:))
Unfortunately
headLens
and
tailLens
does not provide a complete toolbox, one cannot change an empty list to a non-empty list with them, for example.

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

[edit] 3.1.1 List lens usage

Suppose that we have a state
s
of type
type S = (Bool, (Int, [Int]))


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

  • listLens :: Lens S [Int]
    edits the complete list.
  • fstLens :: Lens S Bool
    edits the top level constructor of the list:
    False
    corresponds to
    []
    and
    True
    corresponds to
    (:)
    .
  • headLens = fstLens . sndLens :: Lens S Int
    edits the head of the list.
  • tailLens = sndLens . sndLens :: Lens S [Int]
    edits the 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
    listLens
    when the constructor is changed back to
    (:)
    . 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
    s' :: S
    such that
    s
    viewed through
    tailLens
    is the same as
    s'
    viewed through
    listLens
    . Explained on a figure:

ADT.png

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

[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 }
Note that the
y
field is defined twice.

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

data XTag = X1Tag | X2Tag
The definition of
XTag
is kind of inevitable if we would like to edit the constructor tags. We could use
Bool
, but that would not scale to more constructors. We could use
Int
too, but with less static checks from the type system. The definition of the lens toolbox for
X
:
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
    (XTag, (Int, (a, Char)))
    , we could use
    (XTag, (Int, a, Char))
    or
    (XTag, Int, a, Char)
    too. This is an implementation detail.
  • xLens
    remembers the value of
    y
    if we change between the constructor tags. This is the intended behaviour.
  • xLens
    remembers the values of
    v
    and
    z
    fields if we change between the constructor tags. This is the intended behaviour.

[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
X
value, the state of the editor would be
(XTag, (Int, (a, Char)))
, and one could retrive the actual
X
value by
xLens
from the state. The editor would be the composition of the following simpler editors:
  • An elementary editor for
    XTag
    (maybe a combo box or a checkbox) which would be connected to the editor state by
    fstLens
    .
  • An elementary editor for an
    Int
    (maybe a text box or a slider) which would be connected to the editor state by
    fstLens . sndLens
    .
  • An editor for an
    a
    typed value which would be connected to the editor state by
    fstLens . sndLens . sndLens
    .
  • An editor for a
    Char
    (maybe a combo box or a text box or a virtual keyboard) which would be connected to the editor state by
    sndLens . sndLens . sndLens
    .

Now, the intended behaviour is the following:

  • If the user fills in an
    Int
    value for
    y
    , this value should remain the same after changing the
    XTag
    value.
  • The
    a
    value editor should be active only if the
    XTag
    value is
    X1Tag
    .
  • The
    Char
    editor should be active only if the
    XTag
    value is
    X2Tag
    .
  • If the user fills in an
    a
    value for
    z
    when the
    XTag
    value is
    X1Tag
    , and the user changes
    X1Tag
    to
    X2Tag
    and then back to
    X1Tag
    , the
    a
    value should be the same as before (consider a complex value which is hard to re-create). Similar holds for the
    Char
    value.

[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, ... }
Suppose that the set of different field names is
f1 :: s1
,
f2 :: s2
, ...,
fK :: sK
. Let
cij
be equal to
k
iff
xij
is equal to
fk
.

Define an auxiliary enum type for the constructor tags:

data XTag = X1Tag | X2Tag | ... | XMTag
The definition of the lens toolbox for
X
:
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.

Reddit comments