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

renamed homomorphism to morphism

commitae62b2fb256e7bf795ea8e4792596885d49ce98e authorEdwin Brady <edwin.brady@gmail.com> dateSat 9 Mar 2013, 04:40 (14 years ago) parent50fd9b54be6831
3 files changed+24−24
compare with master
unifiedsplit
lib/Control/Arrow.idr+8−8 lib/Control/Category.idr+3−3 lib/Data/Morphisms.idr+13−13
lib/Control/Arrow.idr+8−8
@@ -15,12 +15,12 @@ class Category arr => Arrow (arr : Type -> Type -> Type) 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 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)
18+instance Arrow Morphism where
19+ arrow f = Mor f
20+ first (Mor f) = Mor $ \(a, b) => (f a, b)
21+ second (Mor f) = Mor $ \(a, b) => (a, f b)
22+ (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)
23+ (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)
2424
2525instance Monad m => Arrow (Kleislimorphism m) where
2626 arrow f = Kleisli (return . f)
@@ -30,11 +30,11 @@ instance Monad m => Arrow (Kleislimorphism m) where
3030 second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
3131 return (a, x)
3232
33− (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
33+ (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
3434 y <- g b
3535 return (x, y)
3636
37− (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
37+ (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
3838 y <- g a
3939 return (x, y)
4040
lib/Control/Category.idr+3−3
@@ -8,9 +8,9 @@ class Category (cat : Type -> Type -> Type) where
88 id : cat a a
99 (.) : cat b c -> cat a b -> cat a c
1010
11−instance Category Homomorphism where
12− id = Homo Builtins.id
13− (Homo f) . (Homo g) = Homo (f . g)
11+instance Category Morphism where
12+ id = Mor Builtins.id
13+ (Mor f) . (Mor g) = Mor (f . g)
1414
1515instance Monad m => Category (Kleislimorphism m) where
1616 id = Kleisli (return . id)
lib/Data/Morphisms.idr+13−13
@@ -4,8 +4,8 @@ import Builtins
44
55%access public
66
7−data Homomorphism : Type -> Type -> Type where
8− Homo : (a -> b) -> Homomorphism a b
7+data Morphism : Type -> Type -> Type where
8+ Mor : (a -> b) -> Morphism a b
99
1010data Endomorphism : Type -> Type where
1111 Endo : (a -> a) -> Endomorphism a
@@ -16,22 +16,22 @@ data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where
1616applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
1717applyKleisli (Kleisli f) a = f a
1818
19−applyHomo : Homomorphism a b -> a -> b
20−applyHomo (Homo f) a = f a
19+applyMor : Morphism a b -> a -> b
20+applyMor (Mor f) a = f a
2121
2222applyEndo : Endomorphism a -> a -> a
2323applyEndo (Endo f) a = f a
2424
25−instance Functor (Homomorphism r) where
26− fmap f (Homo a) = Homo (f . a)
25+instance Functor (Morphism r) where
26+ fmap f (Mor a) = Mor (f . a)
2727
28−instance Applicative (Homomorphism r) where
29− pure a = Homo $ const a
30− (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r
28+instance Applicative (Morphism r) where
29+ pure a = Mor $ const a
30+ (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r
3131
32−instance Monad (Homomorphism r) where
33− return a = Homo $ const a
34− (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r
32+instance Monad (Morphism r) where
33+ return a = Mor $ const a
34+ (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
3535
3636instance Semigroup (Endomorphism a) where
3737 (Endo f) <+> (Endo g) = Endo $ g . f
@@ -42,4 +42,4 @@ instance Monoid (Endomorphism a) where
4242infixr 1 ~>
4343
4444(~>) : Type -> Type -> Type
45−a ~> b = Homomorphism a b
45+a ~> b = Morphism a b