IndexedMonad example

Main.hs

-- in reply to http://www.reddit.com/r/haskell/comments/21mja6/make_lllegal_state_transitions_unrepresentable/
-- 
-- We implement a tiny language with three commands: Open, Close, and Get.
-- The first Get after an Open returns 1, the second Get returns 2, and so on.
-- 
-- Get is only valid while the state is open, and
-- Open must always be matched by a Close.
-- We enforce both restrictions via the type system.
-- 
-- There are two valid states: Opened and Closed.
-- The only legal transitions are
--   Closed ---Open--> Opened
--   Opened ---Get---> Opened
--   Opened ---Close-> Closed
-- No other Transitions are representable.
{-# LANGUAGE RebindableSyntax, GADTs #-}

import qualified Prelude as P
import Prelude (Num(..), Functor(..), Int, IO, (.), seq)


-- States, which must be represented as types
-- so that they can appear as type indices.
data Opened
data Closed

-- The only three valid transitions.
data Transition i j a where
    Open  :: Transition Closed Opened ()
    Close :: Transition Opened Closed ()
    Get   :: Transition Opened Opened Int

-- A sequence of valid transitions.
data Program i j a where
    Return :: a -> Program i i a
    Command :: Transition i j a -> Program i j a
    -- The first half of the Program ends in state `j`,
    -- so the rest of the Program must begin in state `j`.
    Bind :: Program i j a -> (a -> Program j k b) -> Program i k b

-- The only three valid commands.
open  = Command Open
close = Command Close
get   = Command Get

-- At runtime, we need to remember the number of times Get has been called,
-- but we only need to remember this while the resource is still Opened.
data Runtime a where
    StateOpened :: Int -> Runtime Opened
    StateClosed :: Runtime Closed

-- Run a well-formed Program which matches each Open with a Close.
-- We don't actually use IO, but to Open a real resource you probably would.
runProgram :: Program Closed Closed a -> IO a
runProgram = fmap P.fst . go StateClosed
  where
    go :: Runtime i -> Program i j a -> IO (a, Runtime j)
    go s (Return x) = P.return (x, s)
    go s (Bind p f) = go s p P.>>= \(x, s') -> go s' (f x)
    go (StateOpened _)  (Command Close) = P.return ((), StateClosed)
    go (StateOpened n)  (Command Get)   = P.return (n,  StateOpened (n + 1))
    go StateClosed      (Command Open)  = P.return ((), StateOpened 1)
    
    -- Since Haskell is lazy, we must also cover the following case,
    -- otherwise we get a "non-exhaustive patterns" warning.
    go x (Command y) = x `seq` y
                         `seq` P.error "expected x or y to be undefined"


-- Use RebindableSyntax to change the types of return and (>>=).
class IndexedMonad m where
    return :: a -> m i i a
    (>>=) :: m i j a -> (a -> m j k b) -> m i k b

-- More definitions required by RebindableSyntax.
t >> p = t >>= (\() -> p)
fail = P.error

-- Program is not a Monad because `m i j` doesn't unify with `m j k`.
-- It is, however, an IndexedMonad.
instance IndexedMonad Program where
    return = Return
    (>>=) = Bind

-- If you try to reorder the operations
-- so that a Get doesn't occur between an Open and a Close, or
-- if Open is not matched by a Close, you get a type error.
program :: Program Closed Closed [Int]
program = do
    open
    x <- get
    y <- get
    close
    return [x, y]  -- [1, 2]

-- |
-- >>> main
-- [1,2]
main :: IO ()
main = runProgram program P.>>= P.print

Here is a version which doesn't simplify IndexedMonad by hardcoding Transition. The differences are:

1. (>>=)'s first argument is an m instead of a Transition.
2. Bind's first argument is a Program instead of a Transition.
3. Program has an extra constructor, Command, which wraps a Transition.
4. runClosed and runOpened have been merged into a single function go.
5. A new GADT called Runtime allows go to either request an Int or no extra value depending on whether the resource is currently Opened or Closed.