"TTD with Idris"-style implementation of the State monad


#1

In Edwin Brady’s “TTD with Idris” an implementation of the state monad is given by

data State : (stateType : Type) -> Type -> Type where
     Get : State stateType stateType
     Put : stateType -> State stateType ()

     Pure : ty -> State stateType ty
     Bind : State stateType a -> (a -> State stateType b) ->
             State stateType b

get : State stateType stateType
get = Get

put : stateType -> State stateType ()
put = Put

mutual
  Functor (State stateType) where
      map func x = do val <- x
                      pure (func val)

  Applicative (State stateType) where
      pure = Pure
      (<*>) f a = do f' <- f
                     a' <- a
                     pure (f' a')

  Monad (State stateType) where
      (>>=) = Bind

runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get st = (st, st)
runState (Put newState) st = ((), newState)

runState (Pure x) st = (x, st)
runState (Bind cmd prog) st = let (val, nextState) = runState cmd st in
                                  runState (prog val) nextState

I know the “standard” implementation of the state monad newtype State s a = State { runState :: s -> (s, a) } (in fact, I have implemented the Monad type class for it as an exercise).

But I would like to have a Haskell “free” implementation which is as close as possible to the Idris one. The closest I got was this:

data State s a where
  Return :: a -> State s a
  Bind :: State s a -> (a -> State s b) -> State s b 
  Get :: State s s
  Put :: s -> State s ()

I am more familiar with Agda’s inductive data types than with Haskell’s GADTs, but it seems to me that Idris’ data State : (stateType : Type) -> Type -> Type and Haskell’s data State s a are different: the stateType is “fixed”, and the “type in the functorial position” can “vary” between constructors (not sure what the exact terminology should be here).

I have attempted to implement the Functor, Applicative, and Monad type classes for this data type, but I couldn’t do it without pattern matching on the four cases (Put, Get, Return, Bind), and even then I was at a loss. It is very elegant how the Idris implementation defines State to be an instance of those three type classes by mutual recursion; does Haskell allow mutually recursive definitions of instances of type classes? If not, how should I define these for the Idris-style State data type?