So I recently came up with this neat idea, in the hope of sharing code between the strict and lazy State
transformer modules:
{-# LANGUAGE FlexibleInstances, DataKinds, KindSignatures #-}
module State where
data Strictness = Strict | Lazy
newtype State (t :: Strictness) s a = State (s -> (s, a))
returnState :: a -> State t s a
returnState x = State $ \s -> (s, x)
instance Monad (State Lazy s) where
return = returnState
State ma >>= amb = State $ \s -> case ma s of
~(s', x) -> runState (amb x) s'
instance Monad (State Strict s) where
return = returnState
State ma >>= amb = State $ \s -> case ma s of
(s', x) -> runState (amb x) s'
get :: State t s s
get = State $ \s -> (s, s)
put :: s -> State t s ()
put s = State $ \_ -> (s, ())
You can see that get
and put
both work without any duplication – no type class instances, no anything – on both the strict and lazy types. However, even though I cover both possible cases for Strictness
, I don't have a Monad instance for State t s a
in general:
-- from http://blog.melding-monads.com/2009/12/30/fun-with-the-lazy-state-monad/
pro :: State t [Bool] ()
pro = do
pro
s <- get
put (True : s)
-- No instance for (Monad (State t [Bool])) arising from a do statement
The following works fine, albeit requiring FlexibleContexts
:
pro :: (Monad (State t [Bool])) => State t [Bool] ()
-- otherwise as before
Then I can instantiate t
at Lazy
or Strict
and run the result and get what I expect. But why do I have to give that context? Is this a conceptual limitation, or a practical one? Is there some reason I'm missing why Monad (State t s a)
actually doesn't hold, or is there just no way to convince GHC of it yet?
(Aside: using the context Monad (State t s)
doesn't work:
Could not deduce (Monad (State t [Bool])) arising from a do statement
from the context (Monad (State t s))
which just confuses me even more. Surely the former is deducible from the latter?)
This is a limitation, but one with good reason: if it did not work that way what would the expected semantics of
runState :: State t s a -> s -> (s,a)
runState (State f) s = f s
example :: s -> a
example = snd $ runState ((State undefined) >> return 1) ()
well, it could be
example = snd $ runState ((State undefined) >>= \_ -> return 1) ()
= snd $ runState (State $ \s -> case undefined s of (s',_) -> (s',1)) ()
= snd $ case undefined () of (s',_) -> (s',1)
= snd $ case undefined of (s',_) -> (s',1)
= snd undefined
= undefined
or it could be
example = snd $ runState ((State undefined) >>= \_ -> return 1) ()
= snd $ runState (State $ \s -> case undefined s of ~(s',_) -> (s',1)) ()
= snd $ case undefined () of ~(s',_) -> (s',1)
= snd $ (undefined,1)
= 1
these are not the same. One option would be to define a function an extra class, like
class IsStrictness t where
bindState :: State t s a -> (a -> State t s b) -> State t s b
and then then define
instance IsStrictness t => Monad (State t s) where
return = returnState
(>>=) = bindState
and instead of defining bindState
as part of IsStrictness
, you can use a singleton
data SingStrictness (t :: Strictness) where
SingStrict :: SingStrictness Strict
SingLazy :: SingStrictness Lazy
class IsStrictness t where
singStrictness :: SingStrictness t
bindState :: IsStrictness t => State t s a -> (a -> State t s b) -> State t s b
bindState ma' amb' = go singStrictness ma' amb' where
go :: SingStrictness t -> State t s a -> (a -> State t s b) -> State t s b
go SingStrict ma amb = ...
go SingLazy ma amb = ...
which can be enhanced even further using the singelton infrastructures from GHC 7.6 instead of the custom class and singleton type. You will end up with
instance SingI t => Monad (State t s)
which is really not so scary. Get used to having lots of SingI _
in your constraint sets. This is how it is going to work for at least a while, and isn't that ugly.
As to why State t [Bool]
is not deducible from State t s
: the problem is that State t s
is in your top level context, which means that s
is quantified at the outermost level. You are defining a function which says "for any t and s such that Monad (State t s) I will give you ...". But, this doesn't say "for any t such that Monad (State t [Bool]) I will give you ...". Sadly, these universally quantified constraints are not so easy in Haskell.