
  0 | ||| A dependently-typed traversable class
  1 | module Data.Traversable.Dependent
  2 | 
  3 | import Control.Applicative.Const
  4 | import public Data.Foldable.Dependent
  5 | import Data.SortedMap.Dependent
  6 | 
  7 | 
  8 | public export
  9 | interface (DepFoldable i t) => DepTraversable (0 i : Type) (0 t : (i -> Type) -> Type) | t where
 10 |   dtraverse : Applicative f => {0 u : i -> Type} -> {0 v : i -> Type} -> ((x : i) -> u x -> f (v x)) -> t u -> f (t v)
 11 | 
 12 | 
 13 | export
 14 | {0 i : Type} -> DepTraversable i (DPair i) where
 15 |   dtraverse k (x ** y) = (MkDPair x) <$> k x y
 16 | 
 17 | %inline
 18 | impl : {0 u,v : i -> Type} -> ((x : i) -> u x -> v x) -> {x : i} -> u x -> v x
 19 | impl f {x} = f x
 20 | 
 21 | export
 22 | DepTraversable k (SortedDMap k) where
 23 |   dtraverse f = traverse (impl f)
 24 | 
 25 | ||| Any traversable is automatically foldable
 26 | depTraversableFoldMap : (DepTraversable i t, Monoid m) => ((x : i) -> v x -> m) -> t v -> m
 27 | depTraversableFoldMap f = let
 28 |   g : (x : i) -> v x -> Const m (v x)
 29 |   g x = MkConst . f x
 30 |   in runConst . dtraverse g
 31 |