title: How to encode possible state transitions in type?
body: <p>I am trying to replicate in Haskell this piece of Idris code, which enforces correct sequencing of actions through types:</p>
  
  <pre><code> data DoorState = DoorClosed | DoorOpen
   data DoorCmd : Type -&gt;
                  DoorState -&gt;
   DoorState -&gt;
                  Type where
        Open : DoorCmd     () DoorClosed DoorOpen
        Close : DoorCmd    () DoorOpen   DoorClosed
        RingBell : DoorCmd () DoorClosed DoorClosed
        Pure : ty -&gt; DoorCmd ty state state
        (&gt;&gt;=) : DoorCmd a state1 state2 -&gt;
                (a -&gt; DoorCmd b state2 state3) -&gt;
                DoorCmd b state1 state3
  </code></pre>
  
  <p>Thanks to overloading of <code>(&gt;&gt;=)</code> operator, one can write monadic code like:</p>
  
  <pre><code>do Ring 
     Open 
     Close
  </code></pre>
  
  <p>but compiler rejects incorrect transitions like:</p>
  
  <pre><code>do Ring
     Open 
     Ring
     Open
  </code></pre>
  
  <p>I have tried to follow this pattern in the following Haskell fragment:</p>
  
  <pre><code> 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 -&gt; DoorCommand b e x
     Bind  :: DoorCommand b e x -&gt; (x -&gt; DoorCommand e f y) -&gt; DoorCommand b f y
  
   instance Functor (DoorCommand b e) where
     f `fmap` c = Bind c (\ x -&gt; Pure (f x))
  
   -- instance Applicative (DoorCommand b e) where
   --    pure    = Pure
   --    f &lt;*&gt; x = Bind f (\ f' -&gt; Bind x (\ x' -&gt; Pure (f' x')))
  
   -- instance Monad (DoorCommand b e) where
   --   return = Pure
   --   (&gt;&gt;=) = Bind
  </code></pre>
  
  <p>But of course this fails: The <code>Applicative</code> and <code>Monad</code> instances cannot be defined correctly as they require two different instances to properly sequence operations. The constructor <code>Bind</code> can be used to enforce proper sequencing but I cannot manage to use the "nicer" do-notation. </p>
  
  <p>How could I write this code to be able to use do-notation, e.g. to prevent invalid sequences of <code>Command</code>s ?</p>