0 | module Monocle.Traversal
 1 |
 2 | import Control.Applicative.Const
 3 | import Control.Monad.Identity
 4 | import Data.List1
 5 | import Data.SnocList
 6 | import Data.Vect
 7 | import Monocle.Fold
 8 | import Monocle.Setter
 9 |
10 | %default total
11 |
12 | ||| A Traversal is the most basic optic unifying a Fold and a Setter.
13 | |||
14 | ||| While an Optional can focus on at most one value, at Traversal
15 | ||| can focus on many values at once. This makes it very useful for
16 | ||| large-scale modifications of many values in a data object.
17 | public export
18 | record Traversal s t a b where
19 |   constructor T
20 |   mapA   : {0 f : _} -> Applicative f => (a -> f b) -> s -> f t
21 |   fold_  : Fold s t a b
22 |   set_   : Setter s t a b
23 |
24 | ||| Convenience alias for monomorphic Traversals, which do not allow
25 | ||| us to change the value and source types.
26 | public export
27 | 0 Traversal' : (s,a : Type) -> Type
28 | Traversal' s a = Traversal s s a a
29 |
30 | --------------------------------------------------------------------------------
31 | --          Interface
32 | --------------------------------------------------------------------------------
33 |
34 | ||| Interface for converting other optics to Traversals.
35 | public export
36 | interface ToTraversal (0 o : Type -> Type -> Type -> Type -> Type) where
37 |   toTraversal : o s t a b -> Traversal s t a b
38 |
39 | public export %inline
40 | ToTraversal Traversal where toTraversal = id
41 |
42 | --------------------------------------------------------------------------------
43 | --          Conversions
44 | --------------------------------------------------------------------------------
45 |
46 | public export %inline
47 | ToFold Traversal where toFold = fold_
48 |
49 | public export %inline
50 | ToSetter Traversal where
51 |   toSetter = set_
52 |
53 | --------------------------------------------------------------------------------
54 | --          Utilities
55 | --------------------------------------------------------------------------------
56 |
57 | public export %inline
58 | (~>) : Traversal s t a b -> Traversal a b c d -> Traversal s t c d
59 | T t1 f1 s1 ~> T t2 f2 s2 = T (t1 . t2) (f1 ~> f2) (s1 ~> s2)
60 |
61 | ||| Adjust the focus of a Traversal with an effectful computation.
62 | export
63 | modifyA : ToTraversal l => Applicative f => l s t a b -> (a -> f b) -> (s -> f t)
64 | modifyA lns fun = mapA (toTraversal lns) fun
65 |
66 | --------------------------------------------------------------------------------
67 | --          Predefined Traversals
68 | --------------------------------------------------------------------------------
69 |
70 | ||| Every `Traversable` trivially gives rise to a Traversal.
71 | public export %inline
72 | traverse_ : Traversable f => Traversal (f a) (f b) a b
73 | traverse_ = T traverse (F foldMap) (S map)
74 |
75 | ||| `traverse_` specialized to lists.
76 | public export %inline
77 | list_ : Traversal (List a) (List b) a b
78 | list_ = traverse_
79 |
80 | ||| `traverse_` specialized to snoclists.
81 | public export %inline
82 | snoclist_ : Traversal (SnocList a) (SnocList b) a b
83 | snoclist_ = traverse_
84 |
85 | ||| `traverse_` specialized to non-empty lists.
86 | public export %inline
87 | list1_ : Traversal (List1 a) (List1 b) a b
88 | list1_ = traverse_
89 |
90 | ||| `traverse_` specialized to vectors.
91 | public export %inline
92 | vect_ : Traversal (Vect n a) (Vect n b) a b
93 | vect_ = traverse_
94 |