git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/lib/Control/Arrow.idr
39 lines 1.4 kB history raw
1module Category.Arrow
3import Data.Morphisms
4import Control.Category
6%access public
8infixr 3 ***
9infixr 3 &&&
11class Category arr => Arrow (arr : Set -> Set -> Set) where
12 arrow : (a -> b) -> arr a b
13 first : arr a b -> arr (a, c) (b, c)
14 second : arr a b -> arr (c, a) (c, b)
15 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
16 (&&&) : arr a b -> arr a b' -> arr a (b, b')
18instance Arrow Homomorphism where
19 arrow f = Homo f
20 first (Homo f) = Homo $ \(a, b) => (f a, b)
21 second (Homo f) = Homo $ \(a, b) => (a, f b)
22 (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
23 (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)
25instance Monad m => Arrow (Kleislimorphism m) where
26 arrow f = Kleisli (return . f)
27 first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a
28 return (x, b)
30 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
31 return (a, x)
33 (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
34 y <- g b
35 return (x, y)
37 (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
38 y <- g a
39 return (x, y)