Covering all the cases of a promoted datatype

Question

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?)

Answer 1

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.