FunctionalDependencies 不统一唯一标识的类型

Question

这是 MonadState 的定义，但问题适用于 class 和 FunctionalDependencies:

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

假设我有一个使用 s 作为类型参数的数据类型和一个使用它的类型 class:

data StateType s = StateType

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

我可以愉快地为此 class 创建一个实例，它可以按预期编译和工作：

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

但我觉得 FunDeps class 中的 s 是多余的，我可以这样定义 class：

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 的情况下它完全有意义，但是当 m 已知时 s 是已知的，所以这是我没有得到的部分。

换句话说，monad m 在 class 头部和函数中统一为相同，因此它应该在实例中唯一标识状态类型 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-cafe 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 是存在的。

无论如何，并非所有问题都丢失了，而且我遇到的问题有一个不错的解决方法。特别是从 class 实例头中删除 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 页面，否则我永远不会找到具有存在类型的示例。

FunctionalDependencies 不统一唯一标识的类型

FunctionalDependencies does not unify on uniquely identified type

haskell

type-families

functional-dependencies