git.iko.soy/Idris-dev
on master help sign in
added subclasses for Arrow
b9de91bJP Smith
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
@@ -37,3 +40,56 @@ instance Monad m => Arrow (Kleislimorphism m) where
37 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
40 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
38 y <- g a
41 y <- g a
39 return (x, y)
42 return (x, y)
43+
44+class Arrow arr => ArrowZero (arr : Type -> Type -> Type) where
45+ zeroArrow : arr a b
46+
47+class ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where
48+ (<#>) : arr a b -> arr a b -> arr a b
49+
50+class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
51+ left : arr a b -> arr (Either a c) (Either b c)
52+
53+ right : arr a b -> arr (Either c a) (Either c b)
54+ right f = arrow swap >>> left f >>> arrow swap where
55+ swap : Either a b -> Either b a
56+ swap (Left x) = Right x
57+ swap (Right x) = Left x
58+
59+ (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
60+ f +++ g = left f >>> right g
61+
62+ (\|/) : arr a b -> arr c b -> arr (Either a c) b
63+ f \|/ g = f +++ g >>> arrow fromEither
64+
65+instance Monad m => ArrowChoice (Kleislimorphism m) where
66+ left f = f +++ (arrow id)
67+ right f = (arrow id) +++ f
68+ f +++ g = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))
69+ (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)
70+
71+class Arrow arr => ArrowApply (arr : Type -> Type -> Type) where
72+ app : arr (arr a b, a) b
73+
74+instance Monad m => ArrowApply (Kleislimorphism m) where
75+ app = Kleisli $ \(Kleisli f, x) => f x
76+
77+data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
78+ MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a
79+
80+runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a
81+runArrowMonad (MkArrowMonad a) = a
82+
83+instance Arrow a => Functor (ArrowMonad a) where
84+ map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f
85+
86+instance Arrow a => Applicative (ArrowMonad a) where
87+ pure x = MkArrowMonad $ arrow $ \_ => x
88+ (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
89+
90+instance ArrowApply a => Monad (ArrowMonad a) where
91+ (MkArrowMonad m) >>= f =
92+ MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
93+
94+class Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where
95+ loop : arr (Pair a c) (Pair b c) -> arr a b