git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/base/Control/Arrow.idr
105 lines 3.6 kB history raw
1module Control.Arrow
3import Data.Morphisms
4import Control.Category
6%access public
8infixr 5 <++>
9infixr 3 ***
10infixr 3 &&&
11infixr 2 +++
12infixr 2 \|/
14class Category arr => Arrow (arr : Type -> Type -> Type) where
15 arrow : (a -> b) -> arr a b
16 first : arr a b -> arr (a, c) (b, c)
18 second : arr a b -> arr (c, a) (c, b)
19 second f = arrow swap >>> first f >>> arrow swap where
20 swap : (x,y) -> (y,x)
21 swap (x,y) = (y,x)
23 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
24 f *** g = first f >>> second g
26 (&&&) : arr a b -> arr a b' -> arr a (b, b')
27 f &&& g = arrow dup >>> f *** g where
28 dup : x -> (x,x)
29 dup x = (x,x)
31instance Arrow Morphism where
32 arrow f = Mor f
33 first (Mor f) = Mor $ \(a, b) => (f a, b)
34 second (Mor f) = Mor $ \(a, b) => (a, f b)
35 (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)
36 (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)
38instance Monad m => Arrow (Kleislimorphism m) where
39 arrow f = Kleisli (return . f)
40 first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a
41 return (x, b)
43 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
44 return (a, x)
46 (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
47 y <- g b
48 return (x, y)
50 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
51 y <- g a
52 return (x, y)
54class Arrow arr => ArrowZero (arr : Type -> Type -> Type) where
55 zeroArrow : arr a b
57class ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where
58 (<++>) : arr a b -> arr a b -> arr a b
60class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
61 left : arr a b -> arr (Either a c) (Either b c)
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
69 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
70 f +++ g = left f >>> right g
72 (\|/) : arr a b -> arr c b -> arr (Either a c) b
73 f \|/ g = f +++ g >>> arrow fromEither
75instance 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)
81class Arrow arr => ArrowApply (arr : Type -> Type -> Type) where
82 app : arr (arr a b, a) b
84instance Monad m => ArrowApply (Kleislimorphism m) where
85 app = Kleisli $ \(Kleisli f, x) => f x
87data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
88 MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a
90runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a
91runArrowMonad (MkArrowMonad a) = a
93instance Arrow a => Functor (ArrowMonad a) where
94 map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f
96instance Arrow a => Applicative (ArrowMonad a) where
97 pure x = MkArrowMonad $ arrow $ \_ => x
98 (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
100instance ArrowApply a => Monad (ArrowMonad a) where
101 (MkArrowMonad m) >>= f =
102 MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app
104class Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where
105 loop : arr (Pair a c) (Pair b c) -> arr a b