@@ -5,8 +5,11 @@ import Control.Category
55
66%access public
77
8+infixr 5 <++>
89infixr 3 ***
910infixr 3 &&&
11+infixr 2 +++
12+infixr 2 \|/
1013
1114class Category arr => Arrow (arr : Type -> Type -> Type) where
1215 arrow : (a -> b) -> arr a b
@@ -47,3 +50,56 @@ instance Monad m => Arrow (Kleislimorphism m) where
4750 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
4851 y <- g a
4952 return (x, y)
53+
54+class Arrow arr => ArrowZero (arr : Type -> Type -> Type) where
55+ zeroArrow : arr a b
56+
57+class ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where
58+ (<++>) : arr a b -> arr a b -> arr a b
59+
60+class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
61+ left : arr a b -> arr (Either a c) (Either b c)
62+
63+ right : arr a b -> arr (Either c a) (Either c b)
64+ right f = arrow swap >>> left f >>> arrow swap where
65+ swap : Either a b -> Either b a
66+ swap (Left x) = Right x
67+ swap (Right x) = Left x
68+
69+ (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
70+ f +++ g = left f >>> right g
71+
72+ (\|/) : arr a b -> arr c b -> arr (Either a c) b
73+ f \|/ g = f +++ g >>> arrow fromEither
74+
75+instance Monad m => ArrowChoice (Kleislimorphism m) where
76+ left f = f +++ (arrow id)
77+ right f = (arrow id) +++ f
78+ f +++ g = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))
79+ (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)
80+
81+class Arrow arr => ArrowApply (arr : Type -> Type -> Type) where
82+ app : arr (arr a b, a) b
83+
84+instance Monad m => ArrowApply (Kleislimorphism m) where
85+ app = Kleisli $ \(Kleisli f, x) => f x
86+
87+data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
88+ MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a
89+
90+runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a
91+runArrowMonad (MkArrowMonad a) = a
92+
93+instance Arrow a => Functor (ArrowMonad a) where
94+ map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f
95+
96+instance Arrow a => Applicative (ArrowMonad a) where
97+ pure x = MkArrowMonad $ arrow $ \_ => x
98+ (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
99+
100+instance ArrowApply a => Monad (ArrowMonad a) where
101+ (MkArrowMonad m) >>= f =
102+ MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
103+
104+class Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where
105+ loop : arr (Pair a c) (Pair b c) -> arr a b