Personal tools

LGtk/ADT lenses

From HaskellWiki

< LGtk(Difference between revisions)
Jump to: navigation, search
m (wording)
m (wording)
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>. These two lenses form a complete 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>:
+
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>
 
<haskell>
Line 9: Line 9:
 
</haskell>
 
</haskell>
   
Similarly, there is a complete 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?
 
Are there a toolbox of lenses for algebraic data types with multiple constructors?

Revision as of 21:20, 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:

Use one lens for each ADT type, with reversed direction.

3.1 Example: List lens

The ADT lens for lists:

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

3.2 Usage

Suppose that we have a state
s
of type
type S = (Bool, (Int, [Int]))
If we view the state through
listLens :: Lens S [Int]
, we see a list of
Int
s. So we can view the list.

We can edit the list with the following lenses:

  • With
    fstLens :: Lens S Bool
    the top level constructor of the list can be viewed and edited:
    False
    corresponds to
    []
    and
    True
    corresponds to
    (:)
    .
  • With
    headLens = fstLens . sndLens :: Lens S Int
    the first element of the list can be viewed and edited. Note that if the top level constructor of the list is
    []
    , the first element 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 certain applications this is the right behaviour.)
  • With
    tailLens = sndLens . sndLens :: Lens S Int
    the tail of the list can be viewed and edited.
Note that for editing 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

How
s'
is created is a related but different question. See LGtk/Semantics#Dependent_reference_creation.

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]