0 | module Data.DFoldable
 1 |
 2 | ||| Dependent version of `Foldable`
 3 | ||| A minimal implementation includes `dfoldr`
 4 | public export
 5 | interface DFoldable (0 f : (t -> Type) -> Type) where
 6 |   -- TODO what about dependent accumulator?
 7 |   ||| Dependent version of `foldr`
 8 |   dfoldr
 9 |      : {0 el : t -> Type}
10 |     -> ({0 x : t} -> el x -> acc -> acc)
11 |     -> acc
12 |     -> f el
13 |     -> acc
14 |
15 |   -- there seems to be a bug, this does not type-check. If you put the
16 |   -- definition of `dfoldl` before `dfoldr`, then `dfoldr` does not type-check
17 |   -- thus a default implementation of `dfoldl` is moved outside the interface
18 |   -- definition
19 |   --||| Dependent version of `foldl`
20 |   --dfoldl
21 |   --   : (impl : DFoldable f)
22 |   --  => {0 el : t -> Type}
23 |   --  -> ({0 x : t} -> acc -> el x -> acc)
24 |   --  -> acc
25 |   --  -> f el
26 |   --  -> acc
27 |   --dfoldl f z tr = dfoldr f' z tr @{impl} where
28 |   --  f' : {0 x : t} -> el x -> acc -> acc
29 |   --  f' el acc = f acc el
30 |
31 | -- separated from the interface definition due to weird errors
32 | ||| Default implementation of `dfoldl`
33 | ||| Separated from the interface definition due to what seems to be a compiler
34 | ||| bug.
35 | public export
36 | dfoldl
37 |    : (impl : DFoldable f)
38 |   => {0 el : t -> Type}
39 |   -> ({0 x : t} -> acc -> el x -> acc)
40 |   -> acc
41 |   -> f el
42 |   -> acc
43 | dfoldl f z tr = dfoldr f' z tr @{impl} where
44 |   f' : {0 x : t} -> el x -> acc -> acc
45 |   f' el acc = f acc el
46 |
47 | -- separated from the interface definition due to weird errors
48 | -- (the errors occur in modules importing this one)
49 | export
50 | dnull : DFoldable f => f el -> Bool
51 | dnull xs = dfoldr {f} {acc = Lazy Bool} (\ _,_ => False) True xs
52 |
53 | -- separated from the interface definition due to weird errors
54 | ||| `DFoldable` version of `foldlM`
55 | export
56 | dfoldlM
57 |    : {0 m : Type -> Type}
58 |   -> {0 el : t -> Type}
59 |   -> DFoldable f
60 |   => Monad m
61 |   => (funcM : {0 x : t} -> acc -> el x -> m acc)
62 |   -> (init : acc)
63 |   -> (input : f el)
64 |   -> m acc
65 | dfoldlM fm a0 = dfoldl {f} {el} (\ma, b => ma >>= flip fm b) (pure a0)
66 |
67 | -- separated from the interface definition due to weird errors
68 | ||| `DFoldable` version of `foldMap`
69 | export
70 | dfoldMap : (impl : DFoldable f) => Monoid m => ({0 x : t} -> a x -> m) -> f a -> m
71 | dfoldMap f = dfoldr ((<+>) . f) neutral @{impl}
72 |