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?