git.iko.soy/Idris-dev
on master help sign in
Clean up Data.Morphisms
cc54b7bhowtonotwin
libs/base/Data/Morphisms.idr+22−29
compare with master
unifiedsplit
@@ -1,54 +1,47 @@
1module Data.Morphisms
1module Data.Morphisms
2
2
3+%default total
3%access public export
4%access public export
4
5
5−data Morphism : Type -> Type -> Type where
6+record Morphism a b where
6− Mor : (a -> b) -> Morphism a b
7+ constructor Mor
7−
8+ applyMor : a -> b
8−data Endomorphism : Type -> Type where
9+infixr 1 ~>
9− Endo : (a -> a) -> Endomorphism a
10−
11−data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where
10+(~>) : Type -> Type -> Type
12− Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b
11+(~>) = Morphism
13−
14−applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
15−applyKleisli (Kleisli f) a = f a
16
12
17−applyMor : Morphism a b -> a -> b
13+record Endomorphism a where
18−applyMor (Mor f) a = f a
14+ constructor Endo
15+ applyEndo : a -> a
19
16
20−applyEndo : Endomorphism a -> a -> a
17+record Kleislimorphism (f : Type -> Type) a b where
21−applyEndo (Endo f) a = f a
18+ constructor Kleisli
19+ applyKleisli : a -> f b
22
20
23−implementation Functor (Morphism r) where
21+Functor (Morphism r) where
24− map f (Mor a) = Mor (f . a)
22+ map f (Mor a) = Mor $ f . a
25
23
26−implementation Applicative (Morphism r) where
24+Applicative (Morphism r) where
27− pure a = Mor $ const a
25+ pure a = Mor $ const a
28 (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
26 (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
29
27
30−implementation Monad (Morphism r) where
28+Monad (Morphism r) where
31 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
29 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
32
30
33−implementation Semigroup (Endomorphism a) where
31+Semigroup (Endomorphism a) where
34 (Endo f) <+> (Endo g) = Endo $ g . f
32 (Endo f) <+> (Endo g) = Endo $ g . f
35
33
36−implementation Monoid (Endomorphism a) where
34+Monoid (Endomorphism a) where
37 neutral = Endo id
35 neutral = Endo id
38
36
39−infixr 1 ~>
40−
41−(~>) : Type -> Type -> Type
42−a ~> b = Morphism a b
43−
44Cast (Endomorphism a) (Morphism a a) where
37Cast (Endomorphism a) (Morphism a a) where
45 cast (Endo f) = Mor f
38 cast (Endo f) = Mor f
46
39
47Cast (Morphism a a) (Endomorphism a) where
40Cast (Morphism a a) (Endomorphism a) where
48 cast (Mor f) = Endo f
41 cast (Mor f) = Endo f
49
42
50−Monad m => Cast (Morphism a (m b)) (Kleislimorphism m a b) where
43+Cast (Morphism a (f b)) (Kleislimorphism f a b) where
51 cast (Mor f) = Kleisli f
44 cast (Mor f) = Kleisli f
52
45
53−Cast (Kleislimorphism m a b) (Morphism a (m b)) where
46+Cast (Kleislimorphism f a b) (Morphism a (f b)) where
54 cast (Kleisli f) = Mor f
47 cast (Kleisli f) = Mor f