Morphisms.idr

module Data.Morphisms

import Builtins

%access public

data Homomorphism : Type -> Type -> Type where
  Homo : (a -> b) -> Homomorphism a b

data Endomorphism : Type -> Type where
  Endo : (a -> a) -> Endomorphism a

data Kleislimorphism : (Type -> Type) -> Type -> Type -> Type where
  Kleisli : Monad m => (a -> m b) -> Kleislimorphism m a b

applyKleisli : Monad m => (Kleislimorphism m a b) -> a -> m b
applyKleisli (Kleisli f) a = f a

applyHomo : Homomorphism a b -> a -> b
applyHomo (Homo f) a = f a

applyEndo : Endomorphism a -> a -> a
applyEndo (Endo f) a = f a

instance Functor (Homomorphism r) where
  fmap f (Homo a) = Homo (f . a)

instance Applicative (Homomorphism r) where
  pure a                = Homo $ const a
  (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r

instance Monad (Homomorphism r) where
  return a       = Homo $ const a
  (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r

instance Semigroup (Endomorphism a) where
  (Endo f) <+> (Endo g) = Endo $ g . f

instance Monoid (Endomorphism a) where
  neutral = Endo id

infixr 1 ~>

(~>) : Type -> Type -> Type
a ~> b = Homomorphism a b