0 | module Control.ApplicativeB

 2 | import Control.FunctorB

 4 | %default total

 6 | public export

 7 | interface FunctorB k t => ApplicativeB k t | t where

 8 |   constructor MkApplicativeB

 9 |   bpure_ : {0 f : _} -> ((0 a : k) -> f a) -> t f

11 |   bprod : {0 f,g : _} -> t f -> t g -> t (\x => (f x, g x))

13 | public export

14 | bpure : {0 f : _} -> ApplicativeB k t => ({0 a : k} -> f a) -> t f

15 | bpure fun = bpure_ (\_ => fun)

17 | public export %inline

18 | bempty : {0 g : k -> Type} -> Alternative f => ApplicativeB k t => t (f . g)

19 | bempty = bpure empty

21 | public export

22 | bzipWith :

23 |      {0 f,g,h : _}

24 |   -> {auto app : ApplicativeB k t}

25 |   -> ({0 a : k} -> f a -> g a -> h a)

26 |   -> t f

27 |   -> t g

28 |   -> t h

29 | bzipWith fun tf tg = bmap (\(x,y) => fun x y) $ bprod tf tg

31 | public export

32 | bzipWith3 :

33 |      {0 f,g,h,i : _}

34 |   -> {auto app : ApplicativeB k t}

35 |   -> ({0 a : k} -> f a -> g a -> h a -> i a)

36 |   -> t f

37 |   -> t g

38 |   -> t h

39 |   -> t i

40 | bzipWith3 fun tf tg th = bmap (\(x,y,z) => fun x y z) $ bprod tf (bprod tg th)

42 | namespace Syntax

43 |   public export %inline

44 |   pure : {0 f : _} -> ApplicativeB k t => ({0 a : k} -> f a) -> t f

45 |   pure = bpure

47 |   public export

48 |   (<*>) :

49 |         {auto app : ApplicativeB k t}

50 |      -> {0 f,g : k -> Type}

51 |      -> t (\x => f x -> g x)

52 |      -> t f

53 |      -> t g

54 |   (<*>) x y = bzipWith id x y