如何使用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

看来不可能。看起来你的“隐含”在 k 中是逆变的，而你想要的函数则不会。

\n\n

我的意思是，如果你有一些奇怪的类MonadFoo m，并且你定义了怎么办

\n\n

type k m = (MonadCo r m, MonadReader Int m, MonadFoo m)\n

\n\n

假设这个类是专门设计的，使得这个类只能有一个实例（好吧，如果你至少不使用的话GeneralizedNewtypeDeriving），一些 monad MMM，它也是MonadCo r和的一个实例MonadReader Int。那么你的类型Constrain k ()可能与 just 同构MMM ()。因此，您想要一个函数MMM () -> MMM ()\xe2\x80\x94 但输入类型MMM ()比您的函数工作所需的要弱得多。您不太可能以这种方式概括您的功能。

\n\n

更新：

\n\n

一些快乐的奥列格，我们有以下代码：

\n\n

{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE DefaultSignatures #-}\n{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE GADTs #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE MultiParamTypeClasses #-}\n{-# LANGUAGE RankNTypes #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeOperators #-}\nmodule Forall where\nimport Control.Monad.Reader\nclass Monad m => MonadCo r m where\nscary ::\n    (forall m. (MonadCo r m, MonadReader Int m) => m ()) ->\n    (forall m. (MonadCo r m, MonadReader Int m) => m ())\nscary = undefined -- here goes your original function\nclass Equals (d1 :: (* -> *) -> *) d2 where\n    equals :: p d2 -> p d1\n    default equals :: p d1 -> p d1\n    equals = id\ndata Dict k (m :: * -> *) where Dict :: k m => Dict k m\ntype Constraint d a = forall m. d m -> m a\ndata (d1 :+: d2) (m :: * -> *) = Plus (d1 m) (d2 m)\nnewtype ConstraintTrans d = ConstraintTrans {runCT :: Constraint d () -> Constraint d ()}\nwarmAndFuzzy ::\n    forall r d.\n    Equals d (Dict (MonadCo r) :+: Dict (MonadReader Int)) =>\n    Constraint d () -> Constraint d ()\nwarmAndFuzzy =\n    let scary\' ::\n            (MonadCo r m, MonadReader Int m)\n            => (forall m\'. (MonadCo r m\', MonadReader Int m\') => m\' ())\n                -> m ()\n        scary\' = scary\n        waf :: Constraint (Dict (MonadCo r) :+: Dict (MonadReader Int)) () ->\n               Constraint (Dict (MonadCo r) :+: Dict (MonadReader Int)) ()\n        waf c (Plus Dict Dict) =\n            let arg :: forall m\'. (MonadCo r m\', MonadReader Int m\') => m\' ()\n                arg = c $ Plus Dict Dict\n            in scary\' arg\n    in runCT $ equals $ ConstraintTrans waf\n

\n