
  0 | module Control.Applicative.Syntax
  1 | 
  2 | --------------------------------------------------------------------------------
  3 | --          mapN etc
  4 | --------------------------------------------------------------------------------
  5 | 
  6 | public export
  7 | map2 : Functor f => Functor g => (a -> b) -> (f . g) a -> (f . g) b
  8 | map2 = map . map
  9 | 
 10 | public export
 11 | map3 :
 12 |   Functor f => Functor g => Functor h =>
 13 |   (a -> b) -> (f . g . h) a -> (f . g . h) b
 14 | map3 = map . map . map
 15 | 
 16 | public export
 17 | map4 :
 18 |   Functor f => Functor g => Functor h => Functor i =>
 19 |   (a -> b) -> (f . g . h . i) a -> (f . g . h . i) b
 20 | map4 = map . map . map . map
 21 | 
 22 | export infixr 4 <$$>, <$$$>, <$$$$>
 23 | export infixl 3 <**>, <***>, <****>
 24 | 
 25 | public export
 26 | (<$$>) : Functor f => Functor g => (a -> b) -> (f . g) a -> (f . g) b
 27 | (<$$>) = map . map
 28 | 
 29 | public export
 30 | (<$$$>) :  Functor f => Functor g => Functor h
 31 |         => (a -> b) -> (f . g . h) a -> (f . g . h) b
 32 | (<$$$>) = map . map . map
 33 | 
 34 | public export
 35 | (<$$$$>) :  Functor f => Functor g => Functor h => Functor i
 36 |          => (a -> b) -> (f . g . h . i) a -> (f . g . h . i) b
 37 | (<$$$$>) = map . map . map . map
 38 | 
 39 | public export
 40 | (<**>) :  Applicative f => Applicative g
 41 |        => (f . g) (a -> b) -> (f . g) a -> (f . g) b
 42 | x <**> y = [| x <*> y |]
 43 | 
 44 | public export
 45 | (<***>) :
 46 |   Applicative f => Applicative g => Applicative h =>
 47 |   (f . g . h) (a -> b) -> (f . g . h) a -> (f . g . h) b
 48 | x <***> y = [| x <**> y |]
 49 | 
 50 | public export
 51 | (<****>) :
 52 |   Applicative f => Applicative g => Applicative h => Applicative i =>
 53 |   (f . g . h . i) (a -> b) -> (f . g . h . i) a -> (f . g . h . i) b
 54 | x <****> y = [| x <***> y |]
 55 | 
 56 | --------------------------------------------------------------------------------
 57 | --          Implementations
 58 | --------------------------------------------------------------------------------
 59 | 
 60 | public export
 61 | record Comp2 (f,g : Type -> Type) (a : Type) where
 62 |   constructor C2
 63 |   c2 : f (g a)
 64 | 
 65 | public export
 66 | Functor f => Functor g => Functor (Comp2 f g) where
 67 |   map f (C2 v) = C2 $ map2 f v
 68 | 
 69 | public export
 70 | Applicative f => Applicative g => Applicative (Comp2 f g) where
 71 |   pure = C2 . pure . pure
 72 |   C2 vf <*> C2 va = C2 $ [| vf <*> va |]
 73 | 
 74 | public export
 75 | Foldable f => Foldable g => Foldable (Comp2 f g) where
 76 |   foldr fun acc (C2 v) =
 77 |     foldr (flip $ foldr fun) acc v
 78 |   foldl fun acc (C2 v) =
 79 |     foldl (foldl fun) acc v
 80 | 
 81 | public export
 82 | Traversable f => Traversable g => Traversable (Comp2 f g) where
 83 |   traverse fun = map C2 . (traverse . traverse) fun . c2
 84 |