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