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(..), Int(..), IO(..))


-- 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
    -- The Transition ends in state `j`,
    -- so the rest of the Program must begin in state `j`.
    Bind :: Transition i j a -> (a -> Program j k b) -> Program i k b

-- Run a well-formed Program which matches each Open with a Close.
runProgram :: Program Closed Closed a -> IO a
runProgram = runClosed
  where
    runClosed :: Program Closed j a -> IO a
    runClosed (Return x)    = P.return x
    runClosed (Bind Open f) = runOpened (f ()) 1
    
    -- We only need to remember the Int while the state is still Opened.
    runOpened :: Program Opened j a -> Int -> IO a
    runOpened (Return x)     _ = P.return x
    runOpened (Bind Close f) s = runClosed (f ())
    runOpened (Bind Get f)   s = runOpened (f s) (s + 1) 


-- Use RebindableSyntax to change the types of return and (>>=).
-- We hardcode Transition to make the rest of the code more concise.
class IndexedMonad m where
    return :: a -> m i i a
    -- (>>=) :: m i j a -> (a -> m j k b) -> m i k b
    (>>=) :: Transition 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