haskell - 如何使用 Data.Constraint 来具体化约束？

Question

我有一个类型的函数

(forall m. (MonadCo r m, MonadReader Int m) => m ())
    -> (forall m. (MonadCo r m, MonadReader Int m) => m ())

(MonadCo是我自己的代表协程单子(monad)的类型类。如果您愿意，您可以考虑使用MonadError e m来代替。问题将是相同的。)

看来我应该能够具体化约束并最终得到一个具有类型签名的函数

(Equals k (MonadCo r, MonadReader Int))
    => (Constrain k ()) -> (Constrain k ())

但我不知道如何在实践中实现这一点。我完全困惑于什么:-和:=>实际上是。我想我还需要一个 Forall1在那里的某个地方，因为我普遍量化 m ，但我不知道它应该放在哪里。

我真正想做的是具体化 forall m. (MonadCo r m, MonadReader Int m)约束。我认为当我这样做时，无论最终出现在左侧，都将自动成为“正确的事情”。

Data.Constraint看起来很强大，但我不知道从哪里开始。

Answer 1

这应该是一个好的开始:

type ReaderAndCo r m = (MonadCo r m, MonadReader Int m)

g :: (forall m . Dict (ReaderAndCo r m) -> m ())
  -> (forall m . Dict (ReaderAndCo r m) -> m ())
g x Dict = f (x Dict)

您可以将 ReaderAndCo 的字典进一步拆分为两个组件，如果您愿望。

为了使其与您问题中的代码更加相似，您可以引入一个额外的同义词:

type Constrain k a = forall m . Dict (k m) -> m a

g :: Constrain (ReaderAndCo r) () -> Constrain (ReaderAndCo r) ()
g x Dict = f (x Dict)

这是你想要实现的目标吗？