git.iko.soy/Idris-dev
on master help sign in
Merge pull request #73 from raichoo/lib

extended morphisms/categories/arrows

commit83fdb4d5721037b94c2aad372190cf11a78a8441 authorEdwin Brady <edwin.brady@gmail.com> dateTue 13 Nov 2012, 03:26 (14 years ago) parentd530abe27df3e0
3 files changed+52−12
compare with master
unifiedsplit
lib/Control/Arrow.idr+17−1 lib/Control/Category.idr+7−3 lib/Data/Morphisms.idr+28−8
lib/Control/Arrow.idr+17−1
@@ -15,9 +15,25 @@ class Category arr => Arrow (arr : Set -> Set -> Set) where
1515 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
1616 (&&&) : arr a b -> arr a b' -> arr a (b, b')
1717
18−instance Arrow Morphism where
18+instance Arrow Homomorphism where
1919 arrow f = Homo f
2020 first (Homo f) = Homo $ \(a, b) => (f a, b)
2121 second (Homo f) = Homo $ \(a, b) => (a, f b)
2222 (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
2323 (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
88 id : cat a a
99 (.) : cat b c -> cat a b -> cat a c
1010
11−instance Category Morphism where
12− id = Homo Builtins.id
13− (Homo f) . (Homo g) = Homo $ Builtins.(.) f g
11+instance Category Homomorphism where
12+ id = Homo Builtins.id
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
1418
1519infixr 1 >>>
1620(>>>) : Category cat => cat a b -> cat b c -> cat a c
lib/Data/Morphisms.idr+28−8
@@ -1,22 +1,42 @@
11module Data.Morphisms
22
3+import Builtins
4+
35%access public
46
5−data Morphism : Set -> Set -> Set where
6− Homo : (a -> b) -> Morphism a b
7+data Homomorphism : Set -> Set -> Set where
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
718
8−($) : Morphism a b -> a -> b
9−(Homo f) $ a = f a
19+applyHomo : Homomorphism a b -> a -> b
20+applyHomo (Homo f) a = f a
1021
11−instance Monad (Morphism r) where
22+applyEndo : Endomorphism a -> a -> a
23+applyEndo (Endo f) a = f a
24+
25+instance Monad (Homomorphism r) where
1226 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
1428
15−instance Applicative (Morphism r) where
29+instance Applicative (Homomorphism r) where
1630 pure a = Homo $ const a
1731 (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r
1832
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+
1939infixr 1 ~>
2040
2141(~>) : Set -> Set -> Set
22−a ~> b = Morphism a b
42+a ~> b = Homomorphism a b