Monad.agda

module Monad where

open import Data.Nat
open import Data.Vec hiding (_>>=_)

record Monad (m : Set -> Set) : Set₁ where
  infixl 1 _>>=_
  field
    pure : ∀ {a : Set} -> a -> m a
    _>>=_ : ∀ {a b : Set} -> m a -> (a -> m b) -> m b

record MonadTrans (t : (Set -> Set) -> Set -> Set) : Set₁ where
  field
    MonadTransMonad : ∀ {m : Set -> Set} -> Monad m -> Monad (t m)
    lift : ∀ {a : Set} {m : Set -> Set} {monad : Monad m} -> m a -> t m a

record Identity (a : Set) : Set where
  constructor Id
  field
    runId : a
open Identity

instance
  MonadIdentity : Monad Identity
  MonadIdentity = record
    { pure = Id
    ; _>>=_ = λ { (Id x) f → f x }
    }

record IdentityT (m : Set -> Set) (a : Set) : Set where
  constructor IdT
  field
    runIdT : m a
open IdentityT

instance
  MonadIdentityT : ∀ {m : Set -> Set} -> {{monad-m : Monad m}} -> Monad (IdentityT m)
  MonadIdentityT {{monad-m}} = record
    { pure = λ x -> IdT (pure x)
    ; _>>=_ = λ { (IdT mx) f → IdT (mx >>= (λ x → runIdT (f x)))}
    } where open Monad monad-m

instance
  MonadTransIdentityT : MonadTrans IdentityT
  MonadTransIdentityT = record
    { MonadTransMonad = λ monad-m → MonadIdentityT {{monad-m}}
    ; lift = IdT
    }

replicateM : ∀ {a : Set} {m : Set -> Set} {{monad : Monad m}} -> (n : ℕ) -> m a -> m (Vec a n)
replicateM {a} {m} {{monad}} n ma = go n
  where
  open Monad monad
  go : (o : ℕ) -> m (Vec a o)
  go zero = pure []
  go (suc n) = ma >>= λ a → go n >>= λ as → pure (a ∷ as)

test : IdentityT Identity (Vec ℕ 0)
test = replicateM 0 (IdT (Id 0))