0 | module Monocle.Getter
 1 |
 2 | import Control.Monad.State
 3 | import Monocle.Fold
 4 |
 5 | %default total
 6 |
 7 | ||| Getters allows us to extract exactly one piece of data of type `a` from
 8 | ||| a source value of type `s`. They are therefore like Folds but with
 9 | ||| stronger guarantees.
10 | |||
11 | ||| Just like Folds and other optics, Getters can be composed sequentially,
12 | ||| and just like Folds, Getters have two additional type parameters
13 | ||| (`t` and `b`), which have no runtime relevance and are only used to
14 | ||| compose them with other optics.
15 | public export
16 | record Getter (s,t,a,b : Type) where
17 |   constructor G
18 |   to_ : s -> a
19 |
20 | ||| Sequential composition of Getters.
21 | public export %inline
22 | (~>) : Getter s t a b -> Getter a b c d -> Getter s t c d
23 | G f ~> G g = G $ g . f
24 | --------------------------------------------------------------------------------
25 | --          Interface
26 | --------------------------------------------------------------------------------
27 |
28 | ||| Interface for converting other optics to Getters.
29 | public export
30 | interface ToGetter (0 o : Type -> Type -> Type -> Type -> Type) where
31 |   toGetter : o s t a b -> Getter s t a b
32 |
33 | public export %inline
34 | ToGetter Getter where toGetter = id
35 |
36 | ||| Use a Getter to extract a piece of data from a source value.
37 | public export %inline
38 | to : ToGetter o => o s t a b -> s -> a
39 | to = to_ . toGetter
40 |
41 | --------------------------------------------------------------------------------
42 | --          Conversions
43 | --------------------------------------------------------------------------------
44 |
45 | public export %inline
46 | ToFold Getter where
47 |   toFold f = F (. to_ f)
48 |
49 | --------------------------------------------------------------------------------
50 | --          State
51 | --------------------------------------------------------------------------------
52 |
53 | ||| View the current state through a `Getter`
54 | export %inline
55 | getST : Monad m => ToGetter o => o s t a b -> StateT s m a
56 | getST g = to g <$> get
57 |
58 | export %inline
59 | withST : Monad m => ToGetter o => o s s a a -> (a -> StateT s m t) -> StateT s m t
60 | withST g f = getST g >>= f
61 |