0 | module Control.Category.Semigroupoid
 1 |
 2 | import Control.Category.Core
 3 | import Data.Morphisms
 4 | import Data.Profunctor.Types
 5 |
 6 | %default total
 7 |
 8 | ------------------------------------------------------------
 9 | -- Interface
10 | ------------------------------------------------------------
11 |
12 | ||| A *semigroupoid* is a category that lacks identity morphisms.
13 | |||
14 | ||| This is the interface-style definition of a semigroupoid. For the
15 | ||| record-style definition, see `Control.Category.Records.SemigroupoidR`.
16 | |||
17 | ||| Laws:
18 | ||| * `(f . g) . h = f . (g . h)`
19 | public export
20 | interface Semigroupoid (0 cat : obj -> obj -> Type) | cat where
21 |   constructor MkSemigroupoid
22 |   (.) : {a,b,c : _} -> cat b c -> cat a b -> cat a c
23 |
24 |
25 | ------------------------------------------------------------
26 | -- Existing Instances
27 | ------------------------------------------------------------
28 |
29 | namespace Semigroupoid
30 |   ||| Convert a category into a semigroupoid.
31 |   public export
32 |   [FromCategory] Category cat => Semigroupoid cat where
33 |     (.) = Core.(.)
34 |
35 |
36 | -- These instances should not be used unless necessary, as they have
37 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
38 | -- and `Kleisli` over base's `Kleislimorphism`.
39 |
40 | public export
41 | Semigroupoid Morphism where
42 |   Mor f . Mor g = Mor (f . g)
43 |
44 | namespace Semigroupoid
45 |   public export
46 |   [Function] Semigroupoid (~~>) where
47 |     (.) = Prelude.(.)
48 |
49 | public export
50 | Monad m => Semigroupoid (Kleislimorphism m) where
51 |   Kleisli f . Kleisli g = Kleisli (f <=< g)
52 |
53 | public export
54 | Monad m => Semigroupoid (Star m) where
55 |   MkStar f . MkStar g = MkStar (f <=< g)
56 |
57 | public export
58 | Semigroupoid Tagged where
59 |   Tag x . Tag _ = Tag x
60 |
61 |