FunctionalDependencies在唯一标识的类型上不统一

Question

这里是MonadState的定义，但问题适用于带有FunctionalDependencies的任何此类：

class Monad m => MonadState s m | m -> s where
...

考虑到我有使用s作为类型参数的数据类型，并且可以使用它的类型类：

data StateType s = StateType

class MonadState s m => FunDeps s m a where
  workWithStateType :: a -> StateType s -> m ()

我可以很高兴地为此类创建一个实例，该实例可以按预期进行编译和工作：

instance (MonadIO m, MonadState s m) => FunDeps s m (IORef (StateType s)) where
  workWithStateType ref a = liftIO $ writeIORef ref a

但是在我看来，s类中的FunDeps是多余的，我可以像这样定义一个类：

class FunDepsProblem m a where
  workWithStateTypeNoCompile :: MonadState s m => a -> StateType s -> m ()

instance (MonadIO m, MonadState s m) => FunDepsProblem m (IORef (StateType s)) where
  ...

问题是我尝试实现它：

instance (MonadIO m, MonadState s m) => FunDepsProblem m (IORef (StateType s)) where
  workWithStateTypeNoCompile ref a = liftIO $ writeIORef ref a

我收到一个编译错误，告诉我它无法统一实例头和函数中的状态标记s：

fun-deps.hs:18:62: error: …
    • Couldn't match type ‘s1’ with ‘s’
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          workWithStateTypeNoCompile :: forall s1.
                                        MonadState s1 m =>
                                        IORef (StateType s) -> StateType s1 -> m ()
        at /path/to/fun-deps.hs:18:3-28
      ‘s’ is a rigid type variable bound by
        the instance declaration
        at /path/to/fun-deps.hs:17:10-78
      Expected type: StateType s
        Actual type: StateType s1
    • In the second argument of ‘writeIORef’, namely ‘a’
      In the second argument of ‘($)’, namely ‘writeIORef ref a’
      In the expression: liftIO $ writeIORef ref a
    • Relevant bindings include
        a :: StateType s1
          (bound at /path/to/fun-deps.hs:18:34)
        ref :: IORef (StateType s)
          (bound at /path/to/fun-deps.hs:18:30)
        workWithStateTypeNoCompile :: IORef (StateType s)
                                      -> StateType s1 -> m ()
          (bound at /path/to/fun-deps.hs:18:3)
   |
Compilation failed.

我知道，当以这种形式定义它时，隐含的forall存在：

  workWithStateTypeNoCompile :: forall s m a . MonadState s m => a -> StateType s -> m ()

因此从技术上讲，它应该对每个s都有效，并且在没有FunctionalDependencies的情况下完全有意义，但是当s已知时，m是已知的，所以这是我不了解的部分。

换句话说，monad m在类头和函数中统一为相同，因此它应在实例头和函数类型中唯一标识状态类型s。所以我的问题是它为什么不统一？有理论上的原因吗？还是根本没有在ghc中实现？

实际上，如果我将MonadState重写为概念上相同的功能，但是使用TypeFamilies而不是FunctionalDependencies，问题似乎就消失了：

class Monad m => MonadStateFamily m where
  type StateToken m :: *

class Family m a where
  familyStateType :: MonadStateFamily m => a -> StateType (StateToken m) -> m ()

instance (MonadIO m, MonadStateFamily m, s ~ StateToken m) => Family m (IORef (StateType s)) where
  familyStateType ref a = liftIO $ writeIORef ref a

Answer 1

显然，这是FunctionalDependencies的已知限制。我从十年前挖出了Haskell咖啡厅message by Manuel Chakravarty，其中提到FunctionalDependencies不适用于存在类型，并提供了一个非常简洁明了的示例：

class F a r | a -> r
instance F Bool Int

data T a = forall b. F a b => MkT b

add :: T Bool -> T Bool -> T Bool
add (MkT x) (MkT y) = MkT (x + y)

上面的示例产生了编译器错误，该错误表明它无法统一唯一标识的类型，本质上是问题的标题。

    • Couldn't match expected type ‘b’ with actual type ‘b1’
      ‘b1’ is a rigid type variable bound by
        a pattern with constructor: MkT :: forall a b. F a b => b -> T a,
        in an equation for ‘add’

这是问题的编译错误，看起来与上面的非常相似。

    • Couldn't match type ‘s1’ with ‘s’
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          workWithStateTypeNoCompile :: forall s1.
                                        MonadState s1 m =>
                                        IORef (StateType s) -> StateType s1 -> m ()

我怀疑这里有完全相同的概念，因为forall上的workWithStateTypeNoCompile，错误中的类型变量s1存在。

在任何情况下都不会全部丢失，并且针对我遇到的问题有一个不错的解决方法。特别是必须从类实例头中删除s，这可以通过newtype实现：

class FunDepsWorks m a where
  workWithStateTypeCompile :: MonadState s m => a s -> StateType s -> m ()

newtype StateTypeRef s = StateTypeRef (IORef (StateType s))

instance MonadIO m => FunDepsWorks m StateTypeRef where
  workWithStateTypeCompile (StateTypeRef ref) a = liftIO $ writeIORef ref a

请注意，a现在是类型为1的类型变量，并应用于s。

感谢Ben Gamari编译了tf vs fd Wiki页面，否则我将永远找不到存在类型的示例。