Skip to content

Instantly share code, notes, and snippets.

@gelisam
Last active August 22, 2022 18:18
Show Gist options
  • Save gelisam/9845116 to your computer and use it in GitHub Desktop.
Save gelisam/9845116 to your computer and use it in GitHub Desktop.
IndexedMonad example
-- 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
@gelisam
Copy link
Author

gelisam commented Mar 30, 2014

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment