实例归纳性作为约束

Question

我试图表达一个给定的想法

\n

instance (MonadTrans t, MonadX m) => MonadX (t m)\n

\n

由此可见，只要所有的都有实例，任何t1 (t2 ... (tn m))也是。但是，当我尝试写下来时，它不起作用：MonadXtxMonadTrans

\n

{-# LANGUAGE BasicallyEverything #-}\n\ndata Dict c where\n  Dict :: c => Dict c\n\nclass (forall m . Monad m => Monad (t m)) => MonadTrans t where\n  lift :: Monad m => m a -> t m a\n\nclass    (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m\ninstance (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m\n\nliftDict :: MonadTrans t => Dict (Foo c m) -> Dict (Foo c (t m))\nliftDict Dict = Dict \n

\n

这会导致以下错误：

\n

    \xe2\x80\xa2 Could not deduce: c (t1 (t m)) arising from a use of \xe2\x80\x98Dict\xe2\x80\x99\n      from the context: MonadTrans t\n        bound by the type signature for:\n                   liftDict :: forall (t :: (* -> *) -> * -> *)\n                                      (c :: (* -> *) -> Constraint) (m :: * -> *).\n                               MonadTrans t =>\n                               Dict (Foo c m) -> Dict (Foo c (t m))\n        at src/Lib.hs:85:1-64\n      or from: Foo c m\n        bound by a pattern with constructor:\n                   Dict :: forall (a :: Constraint). a => Dict a,\n                 in an equation for \xe2\x80\x98liftDict\xe2\x80\x99\n        at src/Lib.hs:86:10-13\n      or from: (MonadTrans t1, Monad (t1 (t m)))\n        bound by a quantified context at src/Lib.hs:1:1\n    \xe2\x80\xa2 In the expression: Dict\n      In an equation for \xe2\x80\x98liftDict\xe2\x80\x99: liftDict Dict = Dict\n    \xe2\x80\xa2 Relevant bindings include\n        liftDict :: Dict (Foo c m) -> Dict (Foo c (t m))\n          (bound at src/Lib.hs:86:1)\n   |\n86 | liftDict Dict = Dict \n

\n

有什么办法让它发挥作用吗？

\n

Answer 1

使用此处给出的稍微简单的定义，您会得到完全相同的错误Foo c m：

 (c m, Monad m, forall t. MonadTrans t => c (t m))
                                      ^^^ don't really need Monad (t m) here

让我们澄清一些变量名称，以便在编写时清楚哪些变量绝对相等，哪些不相等liftDict。

有：

MonadTrans t
    forall m'. Monad m' => Monad (t m')
Foo c m
    c m
    Monad m
    forall t'. MonadTrans t' => c (t' m)

想：

Foo c (t m)
    c (t m)
    Monad (t m)
    forall t''. MonadTrans t'' => c (t'' (t m))

在“想要”类别中，c (t m)很简单——我们应用forall t'. MonadTrans t' => c (t' m)我们的t'~t和MonadTrans t。通过应用到和，这Monad (t m)也很容易。forall m'. Monad m' => Monad (t m')m'~mMonad m

但最后一个……有点棘手！你希望这些排列起来：

Have: forall t' . MonadTrans t'  => c (t'  m    )
Want: forall t''. MonadTrans t'' => c (t'' (t m))

但他们并不完全一致。这里发生的事情是，这m是一个固定的单子，而不是我们可以专门用于我们的新选择的参数t m！好吧，那我们就来争论一下吧。

class    (c m, Monad m, forall m' t . (Monad m', MonadTrans t) => c (t m')) => Foo c m
instance (c m, Monad m, forall m' t . (Monad m', MonadTrans t) => c (t m')) => Foo c m

这可以编译！但它不再说明我们想要什么，因为我们在这里所说的归纳步骤不需要约束c。幸运的是，我们可以将其添加回来，而不会导致它停止编译：

class    (c m, Monad m, forall m' t . (c m', Monad m', MonadTrans t) => c (t m')) => Foo c m
instance (c m, Monad m, forall m' t . (c m', Monad m', MonadTrans t) => c (t m')) => Foo c m

我认为您可能会发现直观地以稍微不同的方式对这些约束进行分组：

class ( (c m, Monad m) -- base case
      , forall m' t. (c m', Monad m', MonadTrans t) => c (t m')
      -- inductive hypothesis
      ) => Foo c m

但请注意：这种情况的Foo实例可能比您最初想象的要少。特别是，对于类型级应用程序来说，对于Foo c实例来说，只能有一个完全通用的实例。c