涵盖所有推广数据类型的情况

Question

所以我最近提出了这个简洁的想法,希望在严格和懒惰的State变压器模块之间共享代码:

{-# 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, ())

您可以在严格和惰性类型上看到get并且put两者都没有任何重复 - 没有类型类实例,没有任何东西.但是,即使我涵盖了两种可能的情况Strictness,我也没有State t s a一般的Monad实例:

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

以下工作正常,虽然要求FlexibleContexts:

pro :: (Monad (State t [Bool])) => State t [Bool] ()
-- otherwise as before

然后,我可以实例t在Lazy或Strict和运行结果,并得到了我所期望的.但为什么我必须提供这种背景？这是一个概念上的限制,还是一个实际限制？有什么理由我错过了为什么Monad (State t s a)实际上没有,或者没有办法说服GHC呢？

(旁白:使用上下文Monad (State t s) 不起作用:

Could not deduce (Monad (State t [Bool])) arising from a do statement from the context (Monad (State t s))

这让我更加困惑.当然前者可以从后者中扣除吗？)

Answer 1

这是一个限制,但有充分的理由:如果它没有那样工作,那么预期的语义是什么

runState :: State t s a -> s -> (s,a)
runState (State f) s = f s

example :: s -> a
example = snd $ runState ((State undefined) >> return 1) ()

好吧,它可能是

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

或者它可能是

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

这些都不一样.一种选择是将函数定义为额外的类,例如

class IsStrictness t where
   bindState :: State t s a -> (a -> State t s b) -> State t s b

然后定义

instance IsStrictness t => Monad (State t s) where
   return = returnState
   (>>=) = bindState

而不是定义bindState为一部分IsStrictness,你可以使用单身

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 = ...

使用GHC 7.6的singelton基础设施而不是自定义类和单一类型可以进一步增强.你最终会得到

instance SingI t => Monad (State t s)

这真的不那么可怕.习惯SingI _在约束集中有很多.这就是它至少工作一段时间的方式,并不是那么难看.

至于为什么State t [Bool]不能从中推导出来State t s:问题在于State t s你的顶层环境,这意味着它s是在最外层进行量化的.你正在定义一个函数,它表示"对于任何t和s,我会给你Monad(State ts)......".但是,这并没有说"因为Monad(State t [Bool])我会给你......".遗憾的是,这些普遍量化的约束在Haskell中并不那么容易.