Personal tools

LGtk/ADT lenses

From HaskellWiki

< LGtk(Difference between revisions)
Jump to: navigation, search
(fill subsection)
(remark: put-put does not hold)
 
(15 intermediate revisions by one user not shown)
Line 11: Line 11:
 
Similarly, there is a toolbox of lenses for records which toolbox contains one lens for each record field.
 
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?
+
'''Question:'''
  +
  +
Is there a toolbox of lenses for an algebraic data type with multiple constructors?
   
 
== Existing solutions ==
 
== Existing solutions ==
Line 20: Line 20:
   
 
<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 47: Line 47:
 
The proposed solution, summarized:
 
The proposed solution, summarized:
   
'''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.'''
+
'''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 descripton of the proposed lens.
+
Let's see specific examples before the generic description of the proposed lens.
   
 
=== Example: List lens ===
 
=== Example: List lens ===
Line 90: Line 90:
 
Remarks:
 
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.
+
* 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:
 
* 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]]
   
On the figure, edges are lenses and nodes are ''references''. One possible definition of references is described 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 a related but separate question. [[LGtk/Semantics#Dependent_reference_creation]] describes a possible solution.
+
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 ===
 
=== Example: ADT with repeated record fields ===
Line 135: Line 135:
 
* <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 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.
 
* <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 ===
 
=== Generic ADT lens ===
   
TODO
+
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 145: Line 161:
 
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