f395de7 · Idris-dev · git.iko.soy

lib/base.ipkg+3−2

compare with master

unifiedsplit

@@ -6,10 +6,11 @@ modules = builtins, prelude, io, system,

6 prelude.algebra, prelude.cast, prelude.nat, prelude.fin,

7 prelude.list, prelude.maybe, prelude.monad, prelude.applicative,

8 prelude.either, prelude.vect, prelude.strings, prelude.char,

9− prelude.heap, prelude.complex,

9+ prelude.heap, prelude.complex, prelude.morphisms,

10

11 network.cgi,

12

13 language.reflection,

14

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