(refine description; add subsections)
Revision as of 21:58, 7 June 2013
1 Problem description
Lenses provide uniform and compositional way to view and edit data structures.For example, one can view and edit pairs with
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:)
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:
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.1.1 List lens usageSuppose that we have a state
type S = (Bool, (Int, [Int]))
We can view and edit the list through the following lenses:
- edits the complete list.listLens :: Lens S [Int]
- edits the top level constructor of the list:fstLens :: Lens S Boolcorresponds toFalseandcorresponds toTrue.(:)
- edits the head of the list.headLens = fstLens . sndLens :: Lens S Int
- edits the tail of the list.tailLens = sndLens . sndLens :: Lens S [Int]
- 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 throughwhen the constructor is changed back tolistLens. 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 such thats' :: Sviewed throughsis the same astailLensviewed throughs'. Explained on a figure:listLens
3.2 Example: ADT with repeated record fields
3.3 Generic ADT lens
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.