module stlc.monad where

open import stlc.type public

data Monad {A : Type} : Type → Set where
  exception : ∀ {E} → Monad (A + E)
  state : ∀ {S} → Monad (S ⇒ (S × A))
  nondeterminism : Monad (list A)
  continuation : ∀ {R} → Monad ((A ⇒ R) ⇒ R)

data SameMonad : ∀ {A B TA TB} → Monad {A} TA → Monad {B} TB → Set where
  exception : ∀ {A B E} → SameMonad (exception {A} {E}) (exception {B} {E})
  state : ∀ {A B S} → SameMonad (state {A} {S}) (state {B} {S})
  nondeterminism : ∀ {A B} → SameMonad (nondeterminism {A}) (nondeterminism {B})
  continuation : ∀ {A B R} → SameMonad (continuation {A} {R}) (continuation {B} {R})

sameMonadTrans : ∀ {A B C TA TB TC} {ma : Monad {A} TA} {mb : Monad {B} TB} {mc : Monad {C} TC} → SameMonad ma mb → SameMonad mb mc → SameMonad ma mc
sameMonadTrans exception exception = exception
sameMonadTrans state state = state
sameMonadTrans nondeterminism nondeterminism = nondeterminism
sameMonadTrans continuation continuation = continuation

getMonadType : ∀ {A TA} → Monad {A} TA → Type
getMonadType {TA = TA} m = TA