0 | module Data.Functor.TraverseSt
 1 |
 2 | import Control.Monad.State
 3 |
 4 | import Data.Colist
 5 | import Data.List.Lazy
 6 |
 7 | %default total
 8 |
 9 | -----------------
10 | --- Interface ---
11 | -----------------
12 |
13 | ||| A particular case of sub-traversability with the state monad.
14 | |||
15 | ||| This is not a full traverse because the final state is not returned.
16 | ||| This allows us to implement this interface for (potentially) infinite data types.
17 | |||
18 | ||| This interface has a law connecting to the `Functor` superinterface:
19 | ||| `traverseSt () $ const $ pure . f` must act as `map f`.
20 | public export
21 | interface Functor f => TraversableSt f where
22 |   traverseSt : s -> (s -> a -> (s, b)) -> f a -> f b
23 |
24 | --------------------------------------
25 | --- Particular universal functions ---
26 | --------------------------------------
27 |
28 | public export %inline
29 | withIndex : TraversableSt f => f a -> f (Nat, a)
30 | withIndex = traverseSt Z $ \n, x => (S n, n, x)
31 |
32 | public export %inline
33 | (.withIndex) : TraversableSt f => f a -> f (Nat, a)
34 | (.withIndex) = withIndex
35 |
36 | ------------------------------------------
37 | --- Implementations for standard types ---
38 | ------------------------------------------
39 |
40 | public export
41 | TraversableSt Stream where
42 |   traverseSt s f (x::xs) = do
43 |     let (s', y) = f s x
44 |     y :: traverseSt s' f xs
45 |
46 | public export
47 | TraversableSt Colist where
48 |   traverseSt _ _ []      = []
49 |   traverseSt s f (x::xs) = do
50 |     let (s', y) = f s x
51 |     y :: traverseSt s' f xs
52 |
53 | public export
54 | TraversableSt LazyList where
55 |   traverseSt _ _ []      = []
56 |   traverseSt s f (x::xs) = do
57 |     let (s', y) = f s x
58 |     y :: traverseSt s' f xs
59 |
60 | public export
61 | Traversable f => TraversableSt f where
62 |   traverseSt s f = evalState s . traverse (ST . pure .: flip f)
63 |