How to encode possible state transitions in type?

Question

I am trying to replicate in Haskell this piece of Idris code, which enforces correct sequencing of actions through types:

 data DoorState = DoorClosed | DoorOpen
 data DoorCmd : Type ->
                DoorState ->
 DoorState ->
                Type where
      Open : DoorCmd     () DoorClosed DoorOpen
      Close : DoorCmd    () DoorOpen   DoorClosed
      RingBell : DoorCmd () DoorClosed DoorClosed
      Pure : ty -> DoorCmd ty state state
      (>>=) : DoorCmd a state1 state2 ->
              (a -> DoorCmd b state2 state3) ->
              DoorCmd b state1 state3

Thanks to overloading of (>>=) operator, one can write monadic code like:

do Ring 
   Open 
   Close

but compiler rejects incorrect transitions like:

do Ring
   Open 
   Ring
   Open

I have tried to follow this pattern in the following Haskell fragment:

 data DoorState = Closed | Opened

 data DoorCommand (begin :: DoorState) (end :: DoorState) a where
   Open  :: DoorCommand 'Closed 'Opened ()
   Close :: DoorCommand 'Opened 'Closed ()
   Ring  :: DoorCommand 'Closed 'Closed ()

   Pure  :: x -> DoorCommand b e x
   Bind  :: DoorCommand b e x -> (x -> DoorCommand e f y) -> DoorCommand b f y

 instance Functor (DoorCommand b e) where
   f `fmap` c = Bind c (\ x -> Pure (f x))

 -- instance Applicative (DoorCommand b e) where
 --    pure    = Pure
 --    f <*> x = Bind f (\ f' -> Bind x (\ x' -> Pure (f' x')))

 -- instance Monad (DoorCommand b e) where
 --   return = Pure
 --   (>>=) = Bind

But of course this fails: The Applicative and Monad instances cannot be defined correctly as they require two different instances to properly sequence operations. The constructor Bind can be used to enforce proper sequencing but I cannot manage to use the "nicer" do-notation.

How could I write this code to be able to use do-notation, e.g. to prevent invalid sequences of Commands ?

Answer 1

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.