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

lib enhancement

commit0bfc0828f1b793bfe7075f5b1436c9c2108ab689 authorEdwin Brady <edwin.brady@gmail.com> dateWed 31 Oct 2012, 14:57 (14 years ago) parent319582e8a86c2a
7 files changed+34−11
compare with master
unifiedsplit
idris.cabal+1 lib/Control/Arrow.idr+3−1 lib/Control/Category.idr+3−1 lib/Data/Morphisms.idr+22 lib/Prelude/Monad.idr+2−1 lib/Prelude/Morphisms.idr−7 lib/base.ipkg+3−1
idris.cabal+1
@@ -51,6 +51,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
5151 lib/Network/*.idr lib/Control/*.idr
5252 lib/Control/Monad/*.idr lib/Language/*.idr
5353 lib/System/Concurrency/*.idr
54+ lib/Data/*.idr
5455 tutorial/examples/*.idr lib/base.ipkg
5556 config.mk
5657 rts/*.c rts/*.h rts/Makefile
lib/Control/Arrow.idr+3−1
@@ -1,8 +1,10 @@
11module Category.Arrow
22
3−import Prelude.Morphisms
3+import Data.Morphisms
44import Control.Category
55
6+%access public
7+
68infixr 3 ***
79infixr 3 &&&
810
lib/Control/Category.idr+3−1
@@ -1,6 +1,8 @@
11module Control.Category
22
3−import Prelude.Morphisms
3+import Data.Morphisms
4+
5+%access public
46
57class Category (cat : Set -> Set -> Set) where
68 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/Monad.idr+2−1
@@ -42,4 +42,5 @@ mapM f xs = sequence (map f xs)
4242mapM_ : Monad m => (a -> m b) -> List a -> m ()
4343mapM_ f xs = sequence_ (map f xs)
4444
45−
45+flatten : Monad m => m (m a) -> m a
46+flatten a = a >>= id
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,
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.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Morphisms,
9+ Prelude.Heap, Prelude.Complex,
1010
1111 Network.Cgi,
1212
@@ -14,5 +14,7 @@ modules = Builtins, Prelude, IO, System,
1414
1515 Language.Reflection,
1616
17+ Data.Morphisms,
18+
1719 Control.Monad.Identity, Control.Monad.State, Control.Category,
1820 Control.Arrow