涵盖提升数据类型的所有情况

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

然后我可以在Lazy 或Strict 实例化t 并运行结果并得到我期望的结果。但是为什么我必须给出这个背景呢？这是一个概念上的限制，还是一个实际的限制？有什么原因我错过了为什么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 中的单例基础设施而不是自定义类和单例类型进一步增强。你最终会得到

instance SingI t => Monad (State t s)

这真的没那么可怕。习惯于在你的约束集中有很多SingI _。这就是它至少可以工作一段时间的方式，而且还没有那么难看。

至于为什么State t [Bool]不能从State t s推导出来：问题是State t s在你的顶层上下文中，这意味着s是在最外层量化的。您正在定义一个函数，它说“对于任何 t 和 s，例如 Monad (State t s) 我会给你......”。但是，这并不是说“对于任何 t 这样的 Monad (State t [Bool]) 我会给你……”。可悲的是，这些普遍量化的约束在 Haskell 中并不容易。