{-# LANGUAGE GADTs #-}
{-| Implement monads by specifying primitive instructions and their operational semantics.

This package is based on the \"The Operational Monad Tutorial\", published in Issue 15 of The Monad.Reader <http://themonadreader.wordpress.com/>.

You are reading the API reference. For more thorough documentation including design and implementation notes as well as a correctness proof, please consult the included @doc/Documentation.html@.

This API reference includes only basic example code. More intricate examples are available in the @doc/examples@ directory.

-}
module Control.Monad.Operational (
    -- * Basic usage
    Program, singleton, Prompt, view,
    -- $example
    
    -- * Monad transformer
    ProgramT, PromptT(..), viewT
    -- $exampleT
    
    ) where

import Control.Monad.Identity
import Control.Monad.Trans
import Control.Applicative

{------------------------------------------------------------------------------
   Program
------------------------------------------------------------------------------}
{-| The abstract data type 'Program instr a' represents programs.

    * The type constructor @instr :: * -> *@ indexes the primitive instructions.
    
    * @a@ is the return type of a program.
    
    @'Program' instr@ is always a monad and
    automatically obeys the monad laws.
-}
type Program instr a = ProgramT instr Identity a

-- | View type for inspecting the first instruction.
--   It has two constructors 'Return' and @:>>=@.
--   (For technical reasons, they are documented at 'PromptT'.)
type Prompt instr a  = PromptT instr Identity a

-- | View function for inspecting the first instruction.
view :: Program instr a -> Prompt instr a
view = runIdentity . viewT

{- $example

/Example/

Stack machine from \"The Operational Monad Tutorial\".

@
    data StackInstruction a where
        Push :: Int -> StackInstruction ()
        Pop  :: StackInstruction Int
@

@
    type StackProgram a = Program StackInstruction a
@

@
    interpret :: StackProgram a -> (Stack Int -> a)
    interpret = eval . view
        where
        eval :: Prompt StackInstruction a -> (Stack Int -> a)
        eval (Push a :>>= is) stack     = interpret (is ()) (a:stack)
        eval (Pop    :>>= is) (a:stack) = interpret (is a ) stack
        eval (Return a)       stack     = a
@

Note that since 'Prompt' is a GADT, the type annotation for @eval@ is mandatory.

-}

{------------------------------------------------------------------------------
    ProgramT - monad transformer
------------------------------------------------------------------------------}
{-| The abstract data type @'ProgramT' instr m a@ represents programs.

    * The type constructor @instr :: * -> *@ indexes the primitive instructions.
    
    * @m@ is the base monad, embedded with 'lift'.

    * @a@ is the return type of a program.
    
    @'ProgramT' instr m@ is a monad transformer and
    automatically obey both the monad and the lifting laws.
-}
data ProgramT instr m a where
    Lift   :: m a -> ProgramT instr m a
    Bind   :: ProgramT instr m b -> (b -> ProgramT instr m a)
           -> ProgramT instr m a
    Instr  :: instr a -> ProgramT instr m a

instance Monad m => Monad (ProgramT instr m) where
    return = Lift . return
    (>>=)  = Bind

instance MonadTrans (ProgramT instr) where
    lift   = Lift

instance Monad m => Functor (ProgramT instr m) where
    fmap   = liftM

instance Monad m => Applicative (ProgramT instr m) where
    pure   = return
    (<*>)  = ap

-- | Program made from a single primitive instruction.
singleton :: instr a -> ProgramT instr m a
singleton = Instr

-- | View type for inspecting the first instruction.
data PromptT instr m a where
    Return :: a -> PromptT instr m a
    (:>>=) :: instr b -> (b -> ProgramT instr m a ) -> PromptT instr m a

-- | View function for inspecting the first instruction.
viewT :: Monad m => ProgramT instr m a -> m (PromptT instr m a)
viewT (Lift m)                = m >>= return . Return
viewT ((Lift m)     `Bind` g) = m >>= viewT . g
viewT ((m `Bind` g) `Bind` h) = viewT (m `Bind` (\x -> g x `Bind` h))
viewT ((Instr i)    `Bind` g) = return (i :>>= g)
viewT (Instr i)               = return (i :>>= return)

{- $exampleT

/Example/

List monad transformer.

@
    data PlusI m a where
        Zero :: PlusI m a
        Plus :: ListT m a -> ListT m a -> PlusI m a
@

@   
    type ListT m a = ProgramT (PlusI m) m a
@

@   
    runList :: Monad m => ListT m a -> m [a]
    runList = eval <=< viewT
        where
        eval :: Monad m => PromptT (PlusI m) m a -> m [a]
        eval (Return x)        = return [x]
        eval (Zero     :>>= g) = return []
        eval (Plus m n :>>= g) =
            liftM2 (++) (runList (m >>= g)) (runList (n >>= g))
@

Note that since 'Prompt' is a GADT, the type annotation for @eval@ is mandatory.

-}