0 | ||| A dependently-typed Withering
 1 | module Data.Withering.Dependent
 2 |
 3 | import Data.Indexed.FixedDep
 4 | import Data.Indexed.Independent
 5 | import Data.Witherable.Dependent
 6 | import Data.Witherable.Indexed
 7 | import Data.Withering
 8 |
 9 |
10 | public export
11 | data DepWithering : (Type -> Type) -> (i : Type) -> (i -> Type) -> (i -> Type) -> Type where
12 |   MkDepWithering : Applicative f
13 |                 => ({0 t : (i -> Type) -> Type} -> (DepWitherable i t) => t u -> f (t v))
14 |                 -> DepWithering f i u v
15 |
16 | export
17 | runDepWither : (DepWitherable i t) => DepWithering f i u v -> t u -> f (t v)
18 | runDepWither (MkDepWithering w) m = w m
19 |
20 | export
21 | depWitherOne : DepWithering f i u v -> (x : i) -> u x -> f (Maybe (v x))
22 | depWitherOne (MkDepWithering w) x y = let
23 |   z : FixDepIndex x Maybe u
24 |   z = WithDepIndex (Just y)
25 |   in unIndex <$> w z
26 |
27 |
28 |
29 | export
30 | preserving : Applicative f => DepWithering f i u u
31 | preserving = MkDepWithering (pure . id)
32 |
33 | export
34 | flushing : Applicative f => DepWithering f i u v
35 | flushing = MkDepWithering (pure . flush)
36 |
37 | export
38 | mapping : Applicative f => ((x : i) -> u x -> v x) -> DepWithering f i u v
39 | mapping f = MkDepWithering (pure . dmap f)
40 |
41 | export
42 | mapMaybeing : Applicative f => ((x : i) -> u x -> Maybe (v x)) -> DepWithering f i u v
43 | mapMaybeing f = MkDepWithering (pure . dmapMaybe f)
44 |
45 | export
46 | traversing : Applicative f => ((x : i) -> u x -> f (v x)) -> DepWithering f i u v
47 | traversing f = MkDepWithering (dtraverse f)
48 |
49 | export
50 | withering : Applicative f => ((x : i) -> u x -> f (Maybe (v x))) -> DepWithering f i u v
51 | withering f = MkDepWithering (dwither f)
52 |
53 |
54 | export
55 | depWithering : Withering f i a b -> DepWithering f i (const a) (const b)
56 | depWithering (MkWithering w) = MkDepWithering (map dep . w @{independentWitherable} . Indep)
57 |