What you're looking for is indeed Atkey's parameterised monad, now more commonly known as the indexed monad.
class IFunctor f where
imap :: (a -> b) -> f i j a -> f i j b
class IFunctor m => IMonad m where
ireturn :: a -> m i i a
(>>>=) :: m i j a -> (a -> m j k b) -> m i k b
IMonad is the class of monad-like things m :: k -> k -> * -> * describing paths through a directed graph of types belonging to the kind k. >>>= binds a computation which takes the type-level state from i to j into a computation which takes it from j to k, returning a bigger computation from i to k. ireturn allows you to lift a pure value into a monadic computation which doesn't change the type-level state.
I'm going to use the indexed free monad to capture the structure of this sort of request-response action, largely because I don't want to have to figure out how to write the IMonad instance for your type myself:
data IFree f i j a where
IReturn :: a -> IFree f i i a
IFree :: f i j (IFree f j k a) -> IFree f i k a
instance IFunctor f => IFunctor (IFree f) where
imap f (IReturn x) = IReturn (f x)
imap f (IFree ff) = IFree $ imap (imap f) ff
instance IFunctor f => IMonad (IFree f) where
ireturn = IReturn
IReturn x >>>= f = f x
IFree ff >>>= f = IFree $ imap (>>>= f) ff
We can build your Door monad for free from the following functor:
data DoorState = Opened | Closed
data DoorF i j next where
Open :: next -> DoorF Closed Opened next
Close :: next -> DoorF Opened Closed next
Ring :: next -> DoorF Closed Closed next
instance IFunctor DoorF where
imap f (Open x) = Open (f x)
imap f (Close x) = Close (f x)
imap f (Ring x) = Ring (f x)
type Door = IFree DoorF
open :: Door Closed Opened ()
open = IFree (Open (IReturn ()))
close :: Door Opened Closed ()
close = IFree (Close (IReturn ()))
ring :: Door Closed Closed ()
ring = IFree (Ring (IReturn ()))
You can open a door, which causes a currently-closed door to become open, close a currently-open door, or ring the bell of a door which remains closed, presumably because the house's occupant doesn't want to see you.
Finally, the RebindableSyntax language extension means we can replace the standard Monad class with our own custom IMonad.
(>>=) = (>>>=)
m >> n = m >>>= const n
return = ireturn
fail = undefined
door :: Door Open Open ()
door = do
close
ring
open
However I notice that you're not really using the binding structure of your monad. None of your building blocks Open, Close or Ring return a value. So I think what you really need is the following, simpler type-aligned list type:
data Path g i j where
Nil :: Path g i i
Cons :: g i j -> Path g j k -> Path g i k
Operationally, Path :: (k -> k -> *) -> k -> k -> * is like a linked list, but it has some extra type-level structure, once again describing a path through a directed graph whose nodes are in k. The elements of the list are edges g. Nil says you can always find a path from a node i to itself and Cons reminds us that a journey of a thousand miles begins with a single step: if you have an edge from i to j and a path from j to k, you can combine them to make a path from i to k. It's called a type-aligned list because the ending type of one element must match the starting type of the next.
On the other side of Curry-Howard Street, if g is a binary logical relation then Path g constructs its reflexive transitive closure. Or, categorically, Path g is the type of morphisms in the free category of a graph g. Composing morphisms in the free category is just (flipped) appending type-aligned lists.
instance Category (Path g) where
id = Nil
xs . Nil = xs
xs . Cons y ys = Cons y (xs . ys)
Then we can write Door in terms of Path:
data DoorAction i j where
Open :: DoorAction Closed Opened
Close :: DoorAction Opened Closed
Ring :: DoorAction Closed Closed
type Door = Path DoorAction
open :: Door Closed Opened
open = Cons Open Nil
close :: Door Opened Closed
close = Cons Close Nil
ring :: Door Closed Closed
ring = Cons Ring Nil
door :: Door Open Open
door = open . ring . close
You don't get do notation (though I think RebindableSyntax does allow you to overload list literals), but building computations with (.) looks like sequencing of pure functions, which I think is a rather good analogy for what you're doing anyway. For me it requires extra brainpower - a rare and precious natural resource - to use indexed monads. It's better to avoid the complexity of monads when a simpler structure will do.
