git.iko.soy/Idris-dev
on master help sign in
simple arrows
commitf395de75c6a76621c16199c713771d05eec6e9cf authorraichoo <raichoo@googlemail.com> dateSat 20 Oct 2012, 02:42 (14 years ago) parent11dd660
4 files changed+46−2
compare with master
unifiedsplit
lib/base.ipkg+3−2 lib/control/arrow.idr+21 lib/control/category.idr+15 lib/prelude/morphisms.idr+7
lib/base.ipkg+3−2
@@ -6,10 +6,11 @@ modules = builtins, prelude, io, system,
66 prelude.algebra, prelude.cast, prelude.nat, prelude.fin,
77 prelude.list, prelude.maybe, prelude.monad, prelude.applicative,
88 prelude.either, prelude.vect, prelude.strings, prelude.char,
9− prelude.heap, prelude.complex,
9+ prelude.heap, prelude.complex, prelude.morphisms,
1010
1111 network.cgi,
1212
1313 language.reflection,
1414
15− control.monad.identity, control.monad.state
15+ control.monad.identity, control.monad.state, control.category,
16+ control.arrow
lib/control/arrow.idrnew file+21
@@ -0,0 +1,21 @@
1+module category.arrow
2+
3+import prelude.morphisms
4+import control.category
5+
6+infixr 3 ***
7+infixr 3 &&&
8+
9+class Category arr => Arrow (arr : Set -> Set -> Set) where
10+ arrow : (a -> b) -> arr a b
11+ first : arr a b -> arr (a, c) (b, c)
12+ second : arr a b -> arr (c, a) (c, b)
13+ (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
14+ (&&&) : arr a b -> arr a b' -> arr a (b, b')
15+
16+instance Arrow Morphism where
17+ arrow f = Homo f
18+ first (Homo f) = Homo $ \(a, b) => (f a, b)
19+ second (Homo f) = Homo $ \(a, b) => (a, f b)
20+ (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
21+ (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)
lib/control/category.idrnew file+15
@@ -0,0 +1,15 @@
1+module control.category
2+
3+import prelude.morphisms
4+
5+class Category (cat : Set -> Set -> Set) where
6+ id : cat a a
7+ (.) : cat b c -> cat a b -> cat a c
8+
9+instance Category Morphism where
10+ id = Homo builtins.id
11+ (Homo f) . (Homo g) = Homo $ builtins.(.) f g
12+
13+infixr 1 >>>
14+(>>>) : Category cat => cat a b -> cat b c -> cat a c
15+f >>> g = g . f
lib/prelude/morphisms.idrnew file+7
@@ -0,0 +1,7 @@
1+module prelude.morphisms
2+
3+data Morphism : Set -> Set -> Set where
4+ Homo : (a -> b) -> Morphism a b
5+
6+($) : Morphism a b -> a -> b
7+(Homo f) $ a = f a