0 | module Control.Arrow
  1 |
  2 | import Control.Category
  3 | import Data.Either
  4 | import Data.Morphisms
  5 |
  6 |
  7 | export infixr 5 <++>
  8 | export infixr 3 ***
  9 | export infixr 3 &&&
 10 | export infixr 2 +++
 11 | export infixr 2 \|/
 12 |
 13 | public export
 14 | interface Category arr => Arrow (0 arr : Type -> Type -> Type) where
 15 |   ||| Converts a function from input to output into a arrow computation.
 16 |   arrow  : (a -> b) -> arr a b
 17 |   ||| Converts an arrow from `a` to `b` into an arrow on pairs, that applies
 18 |   ||| its argument to the first component and leaves the second component
 19 |   ||| untouched, thus saving its value across a computation.
 20 |   first  : arr a b -> arr (a, c) (b, c)
 21 |   ||| Converts an arrow from `a` to `b` into an arrow on pairs, that applies
 22 |   ||| its argument to the second component and leaves the first component
 23 |   ||| untouched, thus saving its value across a computation.
 24 |   second : arr a b -> arr (c, a) (c, b)
 25 |   second f = arrow {arr = arr} swap >>> first f >>> arrow {arr = arr} swap
 26 |     where
 27 |     swap : (x, y) -> (y, x)
 28 |     swap (a, b) = (b, a)
 29 |   ||| A combinator which processes both components of a pair.
 30 |   (***)  : arr a b -> arr a' b' -> arr (a, a') (b, b')
 31 |   f *** g = first f >>> second g
 32 |   ||| A combinator which builds a pair from the results of two arrows.
 33 |   (&&&)  : arr a b -> arr a b' -> arr a (b, b')
 34 |   f &&& g = arrow dup >>> f *** g
 35 |
 36 | public export
 37 | implementation Arrow Morphism where
 38 |   arrow  f            = Mor f
 39 |   first  (Mor f)      = Mor $ \(a, b) => (f a, b)
 40 |   second (Mor f)      = Mor $ \(a, b) => (a, f b)
 41 |   (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)
 42 |   (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)
 43 |
 44 | public export
 45 | implementation Monad m => Arrow (Kleislimorphism m) where
 46 |   arrow f = Kleisli (pure . f)
 47 |   first (Kleisli f) =  Kleisli $ \(a, b) => do x <- f a
 48 |                                                pure (x, b)
 49 |
 50 |   second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
 51 |                                                pure (a, x)
 52 |
 53 |   (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
 54 |                                                         y <- g b
 55 |                                                         pure (x, y)
 56 |
 57 |   (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
 58 |                                                    y <- g a
 59 |                                                    pure (x, y)
 60 |
 61 | public export
 62 | interface Arrow arr => ArrowZero (0 arr : Type -> Type -> Type) where
 63 |   zeroArrow : arr a b
 64 |
 65 | public export
 66 | interface ArrowZero arr => ArrowPlus (0 arr : Type -> Type -> Type) where
 67 |   (<++>) : arr a b -> arr a b -> arr a b
 68 |
 69 | public export
 70 | interface Arrow arr => ArrowChoice (0 arr : Type -> Type -> Type) where
 71 |   left  : arr a b -> arr (Either a c) (Either b c)
 72 |
 73 |   right : arr a b -> arr (Either c a) (Either c b)
 74 |   right f = arrow mirror >>> left f >>> arrow mirror
 75 |
 76 |
 77 |   (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
 78 |   f +++ g = left f >>> right g
 79 |
 80 |   (\|/) : arr a b -> arr c b -> arr (Either a c) b
 81 |   f \|/ g = f +++ g >>> arrow fromEither
 82 |
 83 | public export
 84 | implementation Monad m => ArrowChoice (Kleislimorphism m) where
 85 |   left f                      = f          +++ (arrow id)
 86 |   right f                     = (arrow id) +++ f
 87 |   f           +++ g           = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))
 88 |   (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)
 89 |
 90 | public export
 91 | interface Arrow arr => ArrowApply (0 arr : Type -> Type -> Type) where
 92 |   app : arr (arr a b, a) b
 93 |
 94 | public export
 95 | implementation Monad m => ArrowApply (Kleislimorphism m) where
 96 |   app = Kleisli $ \(Kleisli f, x) => f x
 97 |
 98 | public export
 99 | data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
100 |   MkArrowMonad : (runArrowMonad : arr Unit a) -> ArrowMonad arr a
101 |
102 | public export
103 | runArrowMonad : ArrowMonad arr a -> arr Unit a
104 | runArrowMonad (MkArrowMonad a) = a
105 |
106 | public export
107 | implementation Arrow a => Functor (ArrowMonad a) where
108 |   map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f
109 |
110 | public export
111 | implementation Arrow a => Applicative (ArrowMonad a) where
112 |   pure x = MkArrowMonad $ arrow $ \_ => x
113 |   (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
114 |
115 | public export
116 | implementation ArrowApply a => Monad (ArrowMonad a) where
117 |   (MkArrowMonad m) >>= f =
118 |     MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
119 |
120 | public export
121 | interface Arrow arr => ArrowLoop (0 arr : Type -> Type -> Type) where
122 |   loop : arr (Pair a c) (Pair b c) -> arr a b
123 |
124 | ||| Applying a binary operator to the results of two arrow computations.
125 | public export
126 | liftA2 : Arrow arr => (a -> b -> c) -> arr d a -> arr d b -> arr d c
127 | liftA2 op f g = (f &&& g) >>> arrow (\(a, b) => a `op` b)
128 |