Dependent State monad in idris2

DependentState.idr

data DependentState : Type -> Type -> Type -> Type where
  MakeDependentState : (s' -> (s'', r)) -> DependentState s' s'' r

ret : r -> DependentState s s r
ret r = MakeDependentState $ \s => (s, r)

get : DependentState s s s
get = MakeDependentState $ \s => (s, s)

set : s'' -> DependentState s' s'' ()
set s'' = MakeDependentState $ \s' => (s'', ())

(>>=) : DependentState s'x s''x rx -> (rx -> DependentState s''x s''y ry) -> DependentState s'x s''y ry
(>>=) (MakeDependentState f) g = MakeDependentState $ \s'x_v =>
  let (s''x_v, rx_v) = f s'x_v in
  let (MakeDependentState h) = g rx_v in
  h s''x_v

(>>) : DependentState s'x s''x rx -> DependentState s''x s''y ry -> DependentState s'x s''y ry
(>>) x y = x >>= const y