Personal tools

LGtk/ADT lenses

From HaskellWiki

< LGtk(Difference between revisions)
Jump to: navigation, search
(many changes)
(refine description; add subsections)
Line 82: Line 82:
 
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>.
 
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>.
   
=== Usage ===
+
==== 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 105: Line 105:
 
[[Image:ADT.png]]
 
[[Image:ADT.png]]
   
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 different question. See [[LGtk/Semantics#Dependent_reference_creation]].
+
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.
  +
  +
  +
=== Example: ADT with repeated record fields ===
  +
  +
TODO
  +
  +
=== Generic ADT lens ===
  +
  +
TODO
   
 
== Links and references ==
 
== Links and references ==

Revision as of 21:58, 7 June 2013

Contents

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.

Are there a toolbox of lenses for algebraic data types with multiple constructors?

2 Existing solutions

2.1 Partial lenses

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

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

The flollowing partial lenses are defined for lists:

headLens :: PartialLens [a] a
headLens = (get, set)
 where
  get [] = Nothing
  get (h:t) = Just h
 
  set [] = Nothing
  set (h:t) = Just (:t)
tailLens :: PartialLens [a] [a]
tailLens = (get, set)
 where
  get [] = Nothing
  get (h:t) = Just t
 
  set [] = Nothing
  set (h:t) = Just (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.

2.2 Other solutions

Please help to extend the list of known solutions.

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

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

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
.

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.
  • 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 described in LGtk/Semantics#References. How
s'
can be created and how
s
and
s'
can be kept in sync is a related but separate question. LGtk/Semantics#Dependent_reference_creation describes a possible solution.


3.2 Example: ADT with repeated record fields

TODO

3.3 Generic ADT lens

TODO

4 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]