Haskell：正在进行违反直觉的类型检查

Question

所以我有这些类型：

newtype StateT s m a = StateT {runStateT :: s -> m (a, s)}

data MTa a = FailTa Exception
        | DoneTa {unpackDoneTa :: (a, O)}
        deriving Show

type O = String
type Exception = String
type State = Int

我制作了 (State s m) Functor、Applicative 和 Monad 类的实例，如下所示：

instance (Monad m) => Functor (StateT s m) where
    fmap f t = StateT $ \is -> do
                    ~(a, s) <- runStateT t is
                    return (f a, s)

instance (Monad m) => Applicative (StateT s m) where
    pure = return
    StateT f <*> StateT t = StateT $ \is -> do
        ~(ta, ts) <- t is
        ~(fa, fs) <- f ts
        return (fa ta, fs)

instance (Monad m) => Monad (StateT s m) where
    return a = StateT $ \s -> return (a, s)
    StateT m1 >>= k = StateT $ \s -> do
        ~(a, s1) <- m1 s
        let StateT m2 = k a
        m2 s1

我还制作了 MTa Functor、Applicative 和 Monad 的实例类:

instance Functor MTa where
    _ `fmap` (FailTa e) = FailTa e
    f `fmap` (DoneTa (a, o)) = DoneTa (f a, o)

instance Applicative MTa where
    pure = return
    _ <*> (FailTa e) = FailTa e
    FailTa e <*> _ = FailTa e
    DoneTa (f, x) <*> DoneTa (a, y) = DoneTa (f a, y ++ x)

instance Monad MTa where
    return a = DoneTa (a, "")
    m >>= f = case m of
        FailTa e -> FailTa e
        DoneTa (a, x) -> case (f a) of
            FailTa e1 -> FailTa e1
            DoneTa (b, y) -> DoneTa (b, x ++ y)

然后我有这个功能：

incTaState :: StateT State MTa ()
incTaState = StateT $ \s -> return ((), s+1)

我认为 return ((), s+1) 的计算结果为 DoneTa (((), s+1), "") 是否正确？如果是，那岂不是说明它的类型是MTa ((), State)。为什么 incTaState 类型检查为 StateT State MTa ()？当我在控制台中运行 this: :t DoneTa ((), "") 时，它的计算结果为 DoneTa ((), "") :: MTa ()。我没有正确解释 incTaState 的 return 部分吗？

这个问题几乎可以这样概括：如果 Done ((), "") 类型检查到 MTa ()，那么 incTaState 类型检查到 StateT State MTa () 是怎么回事？ DoneTa (((), s+1), "")、return ((), s+1) 的分辨率、对 MTa (((), State), O) 的类型检查是否使 incTaState 成为 StateT State MTa ((), State) 的类型而不是指定的类型？

请不要啰嗦 (-vvv)。

非常感谢您的考虑。和平

由于我输入了一个三元组，所以删除了下面的内容。谢谢@HTNW。

我怀疑我不是因为当我运行 :t (StateT $ \s -> DoneTa (((), s+1, ""))) 我得到以下错误：

• Couldn't match expected type ‘((a, b), O)’
                  with actual type ‘((), b, [Char])’
• In the first argument of ‘DoneTa’, namely ‘(((), s + 1, ""))’
  In the expression: DoneTa (((), s + 1, ""))
  In the second argument of ‘($)’, namely
    ‘\ s -> DoneTa (((), s + 1, ""))’
• Relevant bindings include s :: b (bound at <interactive>:1:12)

Answer 1

incTaState :: StateT State MTa ()
incTaState = StateT $ \s -> return ((), s+1)
\s -> ((), s+1)          :: State -> ((), State)
-- You were correct
\s -> return ((), s + 1) :: State -> MTa ((), State)
-- The type of that function matches up with StateT
-- We can set s = State, m = MTa, and a = ()
StateT s     m   a  = s     -> m   (a , s    )
StateT State MTa () = State -> MTa ((), State)
-- So:
StateT $ \s -> return ((), s+1) :: StateT State MTa ()
-- QED

当您运行 StateT $ \s -> DoneTa ((), s+1, "") 时，问题是 DoneTa :: (a, String) -> MTa a 有一个 2 元组，但您传递给它的 ((), s + 1, "") :: ((), State, String) 是一个 3 元组。添加更多嵌套：StateT $ \s -> DoneTa (((), s + 1), "")（其中 (((), s + 1), "") :: (((), State), String)，其中包含 2 元组的 2 元组）。

Haskell：正在进行违反直觉的类型检查

Haskell: Counter-intuitive type checking going on

monads

haskell

functional-programming

typechecking

monad-transformers