Commit 5f13d9d6 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Add tests for parameterised monads from Oleg

parent 3bc99c34
{-# OPTIONS -fno-implicit-prelude #-}
-- Haskell98!
-- Tests of the do-notation for the parameterized monads
-- We demonstrate a variable-type state `monadic' transformer
-- and its phantom-type-state relative to enforce the locking protocol
-- (a lock can be released only if it is being held, and acquired only
-- if it is not being held)
-- The tests are based on the code
-- http://okmij.org/ftp/Computation/monads.html#param-monad
-- Please search for DO-NOT-YET
module DoParamM where
import Prelude (const, String, ($), (.), Maybe(..),
Int, fromInteger, succ, pred, fromEnum, toEnum,
(+), Char, (==), Bool(..),
IO, getLine, putStrLn, read, show)
import qualified Prelude
import qualified Control.Monad.State as State
import qualified Control.Monad.Identity as IdM
-- A parameterized `monad'
class Monadish m where
return :: a -> m p p a
fail :: String -> m p p a
(>>=) :: m p q a -> (a -> m q r b) -> m p r b
m1 >> m2 = m1 >>= (const m2)
-- All regular monads are the instances of the parameterized monad
newtype RegularM m p q a = RegularM{unRM :: m a}
instance Prelude.Monad m => Monadish (RegularM m) where
return = RegularM . Prelude.return
fail = RegularM . Prelude.fail
m >>= f = RegularM ((Prelude.>>=) (unRM m) (unRM . f))
-- As a warm-up, we write the regular State computation, with the same
-- type of state throughout. We thus inject Monad.State into the
-- parameterized monad
test1 = State.runState (unRM c) (0::Int) where
c = gget >>= (\v -> gput (succ v) >> return v)
gget :: (State.MonadState s m) => RegularM m s s s
gget = RegularM State.get
gput :: (State.MonadState s m) => s -> RegularM m s s ()
gput = RegularM . State.put
-- (0,1)
-- The same in the do-notation
test1_do = State.runState (unRM c) (0::Int) where
c = do
v <- gget
gput (succ v)
return v
gget :: (State.MonadState s m) => RegularM m s s s
gget = RegularM State.get
gput :: (State.MonadState s m) => s -> RegularM m s s ()
gput = RegularM . State.put
-- (0,1)
-- Introduce the variable-type state (transformer)
newtype VST m si so v = VST{runVST:: si -> m (so,v)}
instance Prelude.Monad m => Monadish (VST m) where
return x = VST (\si -> Prelude.return (si,x))
fail x = VST (\si -> Prelude.fail x)
m >>= f = VST (\si -> (Prelude.>>=) (runVST m si)
(\ (sm,x) -> runVST (f x) sm))
vsget :: Prelude.Monad m => VST m si si si
vsget = VST (\si -> Prelude.return (si,si))
vsput :: Prelude.Monad m => so -> VST m si so ()
vsput x = VST (\si -> Prelude.return (x,()))
-- Repeat test1 via VST: the type of the state is the same
vsm1 () = vsget >>= (\v -> vsput (succ v) >> return v)
-- The same with the do-notation
vsm1_do () = do
v <- vsget
vsput (succ v)
return v
{-
*DoParamM> :t vsm1
vsm1 :: (Monadish (VST m), IdM.Monad m, Prelude.Enum si) =>
() -> VST m si si si
-}
test2 = IdM.runIdentity (runVST (vsm1 ()) (0::Int))
-- (1,0)
test2_do = IdM.runIdentity (runVST (vsm1_do ()) (0::Int))
-- (1,0)
-- Now, we vary the type of the state, from Int to a Char
vsm2 () = vsget >>= (\v -> vsput ((toEnum (65+v))::Char) >>
vsget >>= \v' -> return (v,v'))
{-
*DoParamM> :t vsm2
vsm2 :: (Monadish (VST m), IdM.Monad m) => () -> VST m Int Char (Int, Char)
-}
-- The same with the do-notation
-- the following does not yet work
vsm2_do () = do
v <- vsget
vsput ((toEnum (65+v))::Char)
v' <- vsget
return (v,v')
test3 = IdM.runIdentity (runVST (vsm2 ()) (0::Int))
-- ('A',(0,'A'))
test3_do = IdM.runIdentity (runVST (vsm2_do ()) (0::Int))
-- ('A',(0,'A'))
{- The following is a deliberate error:
DoParamM.hs:147:55:
Couldn't match expected type `Int' against inferred type `Char'
In the second argument of `(==)', namely `v''
In the first argument of `return', namely `(v == v')'
In the expression: return (v == v')
vsm3 () = vsget >>= (\v -> vsput ((toEnum (65+v))::Char) >>
vsget >>= \v' -> return (v==v'))
-}
-- The following too must report a type error -- the expression
-- return (v == v') must be flagged, rather than something else
vsm3_do () = do
v <- vsget
vsput ((toEnum (65+v))::Char)
v' <- vsget
return (v==v')
-- Try polymorphic recursion, over the state.
-- crec1 invokes itself, and changes the type of the state from
-- some si to Bool.
crec1 :: (Prelude.Enum si, Prelude.Monad m) => VST m si si Int
crec1 = vsget >>= (\s1 -> case fromEnum s1 of
0 -> return 0
1 -> vsput (pred s1) >> return 1
_ -> vsput True >>
crec1 >>= (\v ->
(vsput s1 >> -- restore state type to si
return (v + 10))))
-- The same in the do-notation
crec1_do :: (Prelude.Enum si, Prelude.Monad m) => VST m si si Int
crec1_do = do
s1 <- vsget
case fromEnum s1 of
0 -> return 0
1 -> do {vsput (pred s1); return 1}
_ -> do
vsput True
v <- crec1_do
vsput s1 -- restore state type to si
return (v + 10)
test4 = IdM.runIdentity (runVST crec1 'a')
-- ('a',11)
test4_do = IdM.runIdentity (runVST crec1_do 'a')
-- ('a',11)
-- Another example, to illustrate locking and static reasoning about
-- the locking state
data Locked = Locked; data Unlocked = Unlocked
newtype LIO p q a = LIO{unLIO::IO a}
instance Monadish LIO where
return = LIO . Prelude.return
m >>= f = LIO ((Prelude.>>=) (unLIO m) (unLIO . f))
lput :: String -> LIO p p ()
lput = LIO . putStrLn
lget :: LIO p p String
lget = LIO getLine
-- In the real program, the following will execute actions to acquire
-- or release the lock. Here, we just print out our intentions.
lock :: LIO Unlocked Locked ()
lock = LIO (putStrLn "Lock")
unlock :: LIO Locked Unlocked ()
unlock = LIO (putStrLn "UnLock")
-- We should start in unlocked state, and finish in the same state
runLIO :: LIO Unlocked Unlocked a -> IO a
runLIO = unLIO
-- User code
tlock1 = lget >>= (\l ->
return (read l) >>= (\x ->
lput (show (x+1))))
tlock1r = runLIO tlock1
-- the same in the do-notation
tlock1_do = do
l <- lget
let x = read l
lput (show (x+1))
{-
*VarStateM> :t tlock1
tlock1 :: LIO p p ()
Inferred type has the same input and output states and is polymorphic:
tlock1 does not affect the state of the lock.
-}
tlock2 = lget >>= (\l ->
lock >> (
return (read l) >>= (\x ->
lput (show (x+1)))))
tlock2_do = do
l <- lget
lock
let x = read l
lput (show (x+1))
{-
*VarStateM> :t tlock2
tlock2 :: LIO Unlocked Locked ()
The inferred type says that the computation does the locking.
-}
tlock3 = tlock2 >> unlock
tlock3r = runLIO tlock3
{-
*DoParamM> :t tlock3
tlock3 :: LIO Unlocked Unlocked ()
-}
{-
*DoParamM> tlock3r
-- user input: 123
Lock
124
UnLock
-}
tlock3_do = do {tlock2_do; unlock}
tlock3r_do = runLIO tlock3_do
-- An attempt to execute the following
-- tlock4 = tlock2 >> tlock2
{-
gives a type error:
Couldn't match expected type `Locked'
against inferred type `Unlocked'
Expected type: LIO Locked r b
Inferred type: LIO Unlocked Locked ()
In the expression: tlock2
In a lambda abstraction: \ _ -> tlock2
The error message correctly points out an error of acquiring an already
held lock.
-}
-- The following too must be an error: with the SAME error message as above
tlock4_do = do {tlock2_do; tlock2_do}
-- Similarly, the following gives a type error because of an attempt
-- to release a lock twice
-- tlock4' = tlock2 >> unlock >> unlock
{-
DoParamM.hs:298:30:
Couldn't match expected type `Unlocked'
against inferred type `Locked'
Expected type: LIO Unlocked r b
Inferred type: LIO Locked Unlocked ()
In the second argument of `(>>)', namely `unlock'
In the expression: (tlock2 >> unlock) >> unlock
-}
-- The following too must be an error: with the SAME error message as above
tlock4'_do = do {tlock2_do; unlock; unlock}
DoParamM.hs:146:17:
Couldn't match expected type `Int' against inferred type `Char'
In the second argument of `(==)', namely `v''
In the first argument of `return', namely `(v == v')'
In the expression: return (v == v')
DoParamM.hs:286:27:
Couldn't match expected type `Locked'
against inferred type `Unlocked'
Expected type: LIO Locked r b
Inferred type: LIO Unlocked Locked ()
In the expression: tlock2_do
In the expression:
do tlock2_do
tlock2_do
DoParamM.hs:302:36:
Couldn't match expected type `Unlocked'
against inferred type `Locked'
Expected type: LIO Unlocked r b
Inferred type: LIO Locked Unlocked ()
In the expression: unlock
In the expression:
do tlock2_do
unlock
unlock
{-# OPTIONS -fglasgow-exts -fno-implicit-prelude #-}
-- Tests of the do-notation for the restricted monads
-- We demonstrate that all ordinary monads are restricted monads,
-- and show the frequently requested implementation
-- of MonadPlus in terms of Data.Set.
--
-- The tests are based on the code
-- http://okmij.org/ftp/Haskell/types.html#restricted-datatypes
module DoRestrictedM where
import List
import Prelude (const, String, ($), (.), Maybe(..))
import qualified Prelude
import qualified Data.Set as Set
-- Defining the restricted monad
class MN2 m a where
return :: a -> m a
fail :: String -> m a
class (MN2 m a, MN2 m b) => MN3 m a b where
(>>=) :: m a -> (a -> m b) -> m b
m1 >> m2 = m1 >>= (const m2)
-- All regular monads are the instances of the restricted monad
newtype RegularM m a = RegularM{unRM :: m a}
instance Prelude.Monad m => MN2 (RegularM m) a where
return = RegularM . Prelude.return
fail = RegularM . Prelude.fail
instance Prelude.Monad m => MN3 (RegularM m) a b where
m >>= f = RegularM ((Prelude.>>=) (unRM m) (unRM . f))
-- We try to inject Maybe (as the regular monad) into Restricted Monad
test1s () = return "a" >>= (\x -> return $ "b" ++ x)
test1f () = fail "" >>= (\x -> return $ "b" ++ x)
-- the same with the do-notation
test1s_do () = do
x <- return "a"
return $ "b" ++ x
{-
whose inferred type is
*DoRestrictedM> :t test1s
test1s :: (MN3 m [Prelude.Char] [Prelude.Char]) => () -> m [Prelude.Char]
-}
test1sr :: Maybe String
test1sr = unRM $ test1s ()
-- Just "ba"
test1fr :: Maybe String
test1fr = unRM $ test1f ()
-- Nothing
test1sr_do :: Maybe String
test1sr_do = unRM $ test1s_do ()
-- Just "ba"
-- As often requested, we implement a MonadPlus `monad'
-- in terms of a Set. Set requires the Ord constraint.
newtype SMPlus a = SMPlus{unSM:: Set.Set a}
instance MN2 SMPlus a where
return = SMPlus . Set.singleton
fail x = SMPlus $ Set.empty
instance Prelude.Ord b => MN3 SMPlus a b where
m >>= f = SMPlus (Set.fold (Set.union . unSM . f) Set.empty (unSM m))
-- We cannot forget the Ord constraint, because the typechecker
-- will complain (and tell us exactly what we have forgotten).
-- Now we can instantiate the previously written test1s and test1d
-- functions for this Set monad:
test2sr :: Set.Set String
test2sr = unSM $ test1s ()
-- fromList ["ba"]
test2fr :: Set.Set String
test2fr = unSM $ test1f ()
-- fromList []
test2sr_do :: Set.Set String
test2sr_do = unSM $ test1s_do ()
-- fromList ["ba"]
......@@ -17,3 +17,7 @@ test('rebindable7', normal, compile_and_run, [''])
test('rebindable8', if_compiler_lt('ghc', '6.9', expect_broken(1537)),
compile, [''])
test('rebindable9', expect_broken(1537), compile, [''])
# Tests from Oleg
test('DoRestrictedM', normal, compile, [''])
test('DoParamM', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment