0 | module Control.TraversableB

 2 | import Control.Applicative.Const

 3 | import Control.FunctorB

 5 | %default total

 7 | public export

 8 | interface FunctorB k t => TraversableB k t | t where

 9 |   constructor MkTraversableB

10 |   btraverse_ :

11 |        {0 f,g : _}

12 |     -> {auto app : Applicative e}

13 |     -> ((0 a : k) -> f a -> e (g a))

14 |     -> t f -> e (t g)

16 | public export

17 | btraverse :

18 |      {0 f,g : _}

19 |   -> {auto app : Applicative e}

20 |   -> {auto trv : TraversableB k t}

21 |   -> ({0 a : k} -> f a -> e (g a))

22 |   -> t f -> e (t g)

23 | btraverse fun = btraverse_ (\_ => fun)

25 | public export

26 | bsequence :

27 |      {0 f : _}

28 |   -> {auto app : Applicative e}

29 |   -> {auto trv : TraversableB k t}

30 |   -> t (e . f)

31 |   -> e (t f)

32 | bsequence = btraverse_ (\_,x => x)

34 | public export

35 | bsequence' : Applicative e => TraversableB Type t => t e -> e (t I)

36 | bsequence' = btraverse_ (\_,x => x)

38 | public export

39 | bfoldMap :

40 |      {0 f : _}

41 |   -> {auto app : Monoid m}

42 |   -> {auto trv : TraversableB k t}

43 |   -> ({0 a : k} -> f a -> m)

44 |   -> t f

45 |   -> m

46 | bfoldMap g b = runConst $ btraverse {g = f} (MkConst . g) b