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

但我觉得 FunDeps 类中的 s 是多余的，我可以这样定义一个类:

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

我怀疑这里使用的是完全相同的概念，因为 workWithStateTypeNoCompile 上的 forall，类型变量 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 页面，否则我永远不会找到具有存在类型的示例。