Difference between revisions of "LGtk/ADT lenses"
(many changes) |
|||
Line 57: | Line 57: | ||
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.''' |
||
− | '''Use one lens for each ADT type, with reversed direction.''' |
||
+ | |||
+ | Let's see specific examples before the generic descripton of the proposed lens. |
||
=== Example: List lens === |
=== Example: List lens === |
||
Line 77: | Line 79: | ||
set (l: r) _ = (True, (l, r)) |
set (l: r) _ = (True, (l, r)) |
||
</haskell> |
</haskell> |
||
+ | |||
+ | 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 === |
=== Usage === |
||
Line 86: | Line 90: | ||
</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 |
+ | We can view and edit the list through the following lenses: |
+ | |||
+ | * <hask>listLens :: Lens S [Int]</hask> edits the '''complete list'''. |
||
⚫ | |||
⚫ | |||
+ | * <hask>tailLens = sndLens . sndLens :: Lens S [Int]</hask> edits the '''tail''' of the list. |
||
+ | Remarks: |
||
⚫ | |||
− | * 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.) |
||
⚫ | |||
− | + | * 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. |
|
+ | * 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]] |
||
− | How <hask>s'</hask> |
+ | 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]]. |
== Links and references == |
== Links and references == |
Revision as of 21:48, 7 June 2013
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?
Existing solutions
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.
Other solutions
Please help to extend the list of known solutions.
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.
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
.
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[]
andTrue
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 throughlistLens
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 thats
viewed throughtailLens
is the same ass'
viewed throughlistLens
. Explained on a figure:
How s'
can be created and how s
and s'
can be kept in sync is a related but different question. See LGtk/Semantics#Dependent_reference_creation.
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]