git.iko.soy/Idris-dev
on master help sign in
moved morphisms to lib/Data
2a536ecraichoo
idris.cabal+1
compare with master
unifiedsplit
@@ -51,6 +51,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
51 lib/Network/*.idr lib/Control/*.idr
51 lib/Network/*.idr lib/Control/*.idr
52 lib/Control/Monad/*.idr lib/Language/*.idr
52 lib/Control/Monad/*.idr lib/Language/*.idr
53 lib/System/Concurrency/*.idr
53 lib/System/Concurrency/*.idr
54+ lib/Data/*.idr
54 tutorial/examples/*.idr lib/base.ipkg
55 tutorial/examples/*.idr lib/base.ipkg
55 config.mk
56 config.mk
56 rts/*.c rts/*.h rts/Makefile
57 rts/*.c rts/*.h rts/Makefile
lib/Control/Arrow.idr+3−1
@@ -1,8 +1,10 @@
1module Category.Arrow
1module Category.Arrow
2
2
3−import Prelude.Morphisms
3+import Data.Morphisms
4import Control.Category
4import Control.Category
5
5
6+%access public
7+
6infixr 3 ***
8infixr 3 ***
7infixr 3 &&&
9infixr 3 &&&
8
10
lib/Control/Category.idr+3−1
@@ -1,6 +1,8 @@
1module Control.Category
1module Control.Category
2
2
3−import Prelude.Morphisms
3+import Data.Morphisms
4+
5+%access public
4
6
5class Category (cat : Set -> Set -> Set) where
7class Category (cat : Set -> Set -> Set) where
6 id : cat a a
8 id : cat a a
lib/Data/Morphisms.idrnew file+22
@@ -0,0 +1,22 @@
1+module Data.Morphisms
2+
3+%access public
4+
5+data Morphism : Set -> Set -> Set where
6+ Homo : (a -> b) -> Morphism a b
7+
8+($) : Morphism a b -> a -> b
9+(Homo f) $ a = f a
10+
11+instance Monad (Morphism r) where
12+ return a = Homo $ const a
13+ (Homo h) >>= f = Homo $ \r => f (h r) $ r
14+
15+instance Applicative (Morphism r) where
16+ pure a = Homo $ const a
17+ (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r
18+
19+infixr 1 ~>
20+
21+(~>) : Set -> Set -> Set
22+a ~> b = Morphism a b
lib/Prelude/Morphisms.idrdeleted−7
@@ -1,7 +0,0 @@
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
lib/base.ipkg+3−1
@@ -6,7 +6,7 @@ modules = Builtins, Prelude, IO, System,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Morphisms,
9+ Prelude.Heap, Prelude.Complex,
10
10
11 Network.Cgi,
11 Network.Cgi,
12
12
@@ -14,5 +14,7 @@ modules = Builtins, Prelude, IO, System,
14
14
15 Language.Reflection,
15 Language.Reflection,
16
16
17+ Data.Morphisms,
18+
17 Control.Monad.Identity, Control.Monad.State, Control.Category,
19 Control.Monad.Identity, Control.Monad.State, Control.Category,
18 Control.Arrow
20 Control.Arrow