module Test where

open import Data.Maybe
open import Data.Nat
open import Category.Monad.State

record Monad (M : Set → Set) : Set₁ where
  field
    return : ∀ {A} → A → M A
    _>>=_ : ∀ {A B} → M A → (A → M B) → M B

return : ∀ {A M} {{m : Monad M}} → A → M A
return {{m}} = Monad.return m

_>>=_ : ∀ {A B M} {{m : Monad M}} → M A → (A → M B) → M B
_>>=_ {{m}} = Monad._>>=_ m

_ap_ : ∀ {A B M} {{m : Monad M}} → M (A → B) → M A → M B
mf ap mx = mf >>= (λ f → mx >>= (λ x → return (f x)))

_⋆_ : ∀ {A B M} {{m : Monad M}} → (A → M B) → M A → M B
mf ⋆ mx = mx >>= mf

liftM : ∀ {A B M} {{m : Monad M}} → (A → B) → M A → M B
liftM f mx = mx >>= (λ x → return (f x))

lift2M : ∀ {A B C M} {{m : Monad M}} → (A → B → C) → M A → M B → M C
lift2M f mx my = mx >>= (λ x → my >>= (λ y → return (f x y)))

stateMonad : Monad (State ℕ)
stateMonad = {!!}

maybeMonad : Monad Maybe
maybeMonad = {!!}

postulate
  read : ℕ -> State ℕ (Maybe ℕ)
  write : Maybe ℕ -> State ℕ ℕ

execute : ℕ -> State ℕ ℕ
execute zero = {!!}
execute (suc n) = (execute n >>= read) >>= \ mt -> (execute n >>= read) >>= \ mt' -> write (lift2M _+_ mt mt')