Haskell - Mixed state computation
Given the following structure:
data Computation a = Pure (CState -> (a, CState))
| Action (CState -> IO (a, CState))
(CState is some kind of structure used to store state, but isn't of much interest right now.)
Now I want to make it an instance of Monad, which is basically a state monad and would be easily implemented using StateT. The only addition I have is that I want to keep track of whether the final computation is Pure on or Action, and I want to check if the Computation contains any Action
s, before executing Action
(so IO is Action
not executed).
It should also be noted that it doesn't really matter what the Computation
two constructors have. I've just started implementing this with these constructors.
The rules for determining whether a >> b
Pure is simple:
a >> b
Pure
if a
and b
both Pure
, otherwise this is an action.
Now I started to inject the Monad instance:
instance Monad Computation where
return x = Pure $ \s -> (x, s)
(Action c) >>= f = Action . runStateT $
(StateT $ unpackAction oldComp) >>= (StateT . unpackAction . f)
p@(Pure c) >>= f
| givesPure f = Pure . runState $
state oldF >>= (state . unpackPure . f)
| otherwise = liftComp p >>= f -- Just lift the first argument and recurse, to make an action
-- Helper functions used above:
unpackAction :: Computation a -> (CState -> IO (a, CState))
unpackAction (Pure c) = return . c
unpackAction (Action c) = c
-- Make an Action out of a Pure
liftComp :: Computation a -> Computation a
liftComp (Pure c) = Action $ return . c
liftComp a@(Action _) = a
So the only missing piece is the function givesPure
and I'm not sure if it can even be implemented. I once had an implementation like this:
givesPure :: (a -> Computation b) -> Bool
givesPure f = isPure $ f undefined -- I actually used error with a custom message instead of undefined, but that shouldn't matter
isPure :: Computation a -> Bool
isPure (Pure _) = True
isPure (Action _) = False
This works, but makes the assumption that the function I am binding with always returns a computation with the same purity, no matter what the input is. This assumption turned out to be reasonable for me, since the purity of the calculation should be clearly stated and does not depend on some calculations, until I noticed that the function in the following form does not work with this assumption:
baz :: Int -> Computation b
baz x = if x > 5
then foo
else bar
-- foo and bar both have the type Computation b
It seems to me that this cannot be done, as I need the current state to apply the first computation, to get the correct input for the function, to get the second computation and check if it is clean.
Does anyone see a solution to this, or has proof that this is not possible?
source to share
You can try using GADT:
data Pure
data Action
data Computation t a where
Pure :: (CState -> (a, CState)) -> Computation t a
Action :: (CState -> IO (a, CState)) -> Computation Action a
The idea is that the value x :: Computation Action a
can do IO (but can also be pure) and the value y :: Computation Pure a
cannot do IO.
For example,
liftComp :: Computation t a -> Computation Action a
liftComp (Pure c) = Pure c
liftComp x@(Action c) = x
source to share
You are faced with the fact that monadic calculations are not suitable for static analysis, because the effects (in your case, the presence of effects) depend on the values ββobtained during the calculation itself. You cannot predict them without performing calculations.
When you go from Applicative
to Arrow
to Monad
, you gain "power" (you can express more computation), but you lose the ability to statically analyze.
For Applicative
s, there is a ready-made Lift
data type that adds pure computation to an already existing application. But he doesn't have a copy Monad
.
source to share