adjoints.idr

module Modules

data Func a b = MkFunc (a -> b)

interface (Functor f, Functor g) => Adjoint (f : Type -> Type) (g : Type -> Type) where
  unit : a -> g (f a)
  counit : f (g a) -> a

interface Functor f => MyMonad (f : Type -> Type) where
  myjoin : f (f a) -> f a

implementation Functor (Func a) where
  map f (MkFunc g) = MkFunc (f . g)

implementation Functor (Pair a) where
  map f (x, y) = (x, f y)


data Comp : f -> g -> a -> Type where 
  MkComp : (Functor f, Functor g) => (f (g a)) -> Comp f g a

unwrap : Comp f g a -> f (g a)
unwrap (MkComp f) = f

implementation Functor (Comp f g) where
  map f (MkComp x) = MkComp (map (map f) x)

MyState : Type -> Type -> Type
MyState s a = Comp (Func s) (Pair s) a

get : MyState a a
get = MkComp (MkFunc (\x => (x, x)))

set : s -> MyState s ()
set value = MkComp (MkFunc (\_ => (value, ())))

modify : (s -> s) -> MyState s ()
modify f = MkComp (MkFunc (\s => (f s, ())))

run : MyState s result -> s -> result
run (MkComp (MkFunc f)) start = snd (f start)

implementation Adjoint (Pair s) (Func s) where
  unit x = MkFunc (\s => (s, x))
  counit (s, MkFunc f) = f s


implementation Adjoint f g => MyMonad (Comp g f) where
  myjoin (MkComp x) = MkComp (map (counit . map unwrap) x)

implementation Adjoint f g => Applicative (Comp g f) where
  pure x = MkComp (unit x)
  lhs <*> rhs = myjoin (map (\x => map (\y => y x) lhs) rhs)

implementation Adjoint f g => Monad (Comp g f) where
   join (MkComp x) = MkComp (map (counit . map unwrap) x)

example : MyState Int Int
example = do
  set 5
  modify (+ 1)
  get