mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 20:51:43 +03:00
28 lines
697 B
Idris
28 lines
697 B
Idris
|
module Control.Category
|
||
|
|
||
|
import Data.Morphisms
|
||
|
|
||
|
|
||
|
public export
|
||
|
interface Category (cat : Type -> Type -> Type) where
|
||
|
id : cat a a
|
||
|
(.) : cat b c -> cat a b -> cat a c
|
||
|
|
||
|
public export
|
||
|
Category Morphism where
|
||
|
id = Mor id
|
||
|
-- disambiguation needed below, because unification can now get further
|
||
|
-- here with Category.(.) and it's only interface resolution that fails!
|
||
|
(Mor f) . (Mor g) = Mor $ Basics.(.) f g
|
||
|
|
||
|
public export
|
||
|
Monad m => Category (Kleislimorphism m) where
|
||
|
id = Kleisli (pure . id)
|
||
|
(Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
|
||
|
|
||
|
infixr 1 >>>
|
||
|
|
||
|
public export
|
||
|
(>>>) : Category cat => cat a b -> cat b c -> cat a c
|
||
|
f >>> g = g . f
|