git.iko.soy/Idris-dev
on master help sign in
Merge pull request #73 from raichoo/lib
83fdb4dEdwin Brady
lib/Control/Arrow.idr+17−1
compare with master
unifiedsplit
@@ -15,9 +15,25 @@ class Category arr => Arrow (arr : Set -> Set -> Set) where
15 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
15 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
16 (&&&) : arr a b -> arr a b' -> arr a (b, b')
16 (&&&) : arr a b -> arr a b' -> arr a (b, b')
17
17
18−instance Arrow Morphism where
18+instance Arrow Homomorphism where
19 arrow f = Homo f
19 arrow f = Homo f
20 first (Homo f) = Homo $ \(a, b) => (f a, b)
20 first (Homo f) = Homo $ \(a, b) => (f a, b)
21 second (Homo f) = Homo $ \(a, b) => (a, f b)
21 second (Homo f) = Homo $ \(a, b) => (a, f b)
22 (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
22 (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
23 (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)
23 (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)
24+
25+instance 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)
29+
30+ second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
31+ return (a, x)
32+
33+ (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
34+ y <- g b
35+ return (x, y)
36+
37+ (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
38+ y <- g a
39+ return (x, y)
lib/Control/Category.idr+7−3
@@ -8,9 +8,13 @@ class Category (cat : Set -> Set -> Set) where
8 id : cat a a
8 id : cat a a
9 (.) : cat b c -> cat a b -> cat a c
9 (.) : cat b c -> cat a b -> cat a c
10
10
11−instance Category Morphism where
11+instance Category Homomorphism where
12− id = Homo Builtins.id
12+ id = Homo Builtins.id
13− (Homo f) . (Homo g) = Homo $ Builtins.(.) f g
13+ (Homo f) . (Homo g) = Homo (f . g)
14+
15+instance Monad m => Category (Kleislimorphism m) where
16+ id = Kleisli (return . id)
17+ (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
14
18
15infixr 1 >>>
19infixr 1 >>>
16(>>>) : Category cat => cat a b -> cat b c -> cat a c
20(>>>) : Category cat => cat a b -> cat b c -> cat a c
lib/Data/Morphisms.idr+28−8
@@ -1,22 +1,42 @@
1module Data.Morphisms
1module Data.Morphisms
2
2
3+import Builtins
4+
3%access public
5%access public
4
6
5−data Morphism : Set -> Set -> Set where
7+data Homomorphism : Set -> Set -> Set where
6− Homo : (a -> b) -> Morphism a b
8+ Homo : (a -> b) -> Homomorphism a b
9+
10+data Endomorphism : Set -> Set where
11+ Endo : (a -> a) -> Endomorphism a
12+
13+data Kleislimorphism : (Set -> Set) -> Set -> Set -> Set where
14+ Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b
15+
16+applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
17+applyKleisli (Kleisli f) a = f a
7
18
8−($) : Morphism a b -> a -> b
19+applyHomo : Homomorphism a b -> a -> b
9−(Homo f) $ a = f a
20+applyHomo (Homo f) a = f a
10
21
22+applyEndo : Endomorphism a -> a -> a
23+applyEndo (Endo f) a = f a
24+
11−instance Monad (Morphism r) where
25+instance Monad (Homomorphism r) where
12 return a = Homo $ const a
26 return a = Homo $ const a
13− (Homo h) >>= f = Homo $ \r => f (h r) $ r
27+ (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r
14
28
15−instance Applicative (Morphism r) where
29+instance Applicative (Homomorphism r) where
16 pure a = Homo $ const a
30 pure a = Homo $ const a
17 (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r
31 (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r
18
32
33+instance Semigroup (Endomorphism a) where
34+ (Endo f) <+> (Endo g) = Endo $ g . f
35+
36+instance Monoid (Endomorphism a) where
37+ neutral = Endo id
38+
19infixr 1 ~>
39infixr 1 ~>
20
40
21(~>) : Set -> Set -> Set
41(~>) : Set -> Set -> Set
22−a ~> b = Morphism a b
42+a ~> b = Homomorphism a b