git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1795 from japesinator/arrow_classes
0cc80c6Edwin Brady
libs/base/Control/Arrow.idr+56
compare with master
unifiedsplit
@@ -5,8 +5,11 @@ import Control.Category
5
5
6%access public
6%access public
7
7
8+infixr 5 <++>
8infixr 3 ***
9infixr 3 ***
9infixr 3 &&&
10infixr 3 &&&
11+infixr 2 +++
12+infixr 2 \|/
10
13
11class Category arr => Arrow (arr : Type -> Type -> Type) where
14class Category arr => Arrow (arr : Type -> Type -> Type) where
12 arrow : (a -> b) -> arr a b
15 arrow : (a -> b) -> arr a b
@@ -47,3 +50,56 @@ instance Monad m => Arrow (Kleislimorphism m) where
47 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
50 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
48 y <- g a
51 y <- g a
49 return (x, y)
52 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