haskell——n 级约束？ （或者，monad 转换器和 Data.Suitable）

我正在尝试写一些看起来类似于“rank 2 types”的东西，但是为了约束。 （或者，也许假设改变是不正确的->在“rank 2 types”的定义中=>是有意义的；如果您想出更好的术语，请编辑问题）。

setup

首先，Suitable类型类（来自数据合适 http://hackage.haskell.org/packages/archive/suitable/0.1.1/doc/html/Data-Suitable.html， rmonad 的基础）可用于表示可以使用的值的类型。在这个问题中，我将使用

Suitable m a

来表示该值a可以用作 monad 的某些函数的值m（特别是，如果m是DSL，那么它的值通常是a哪些是合适的），例如

class PrintSuitable m where
    printSuitable :: Suitable m a => a -> m ()

请参阅 RMonad 的置顶评论 [link http://hackage.haskell.org/packages/archive/rmonad/0.7/doc/html/Control-RMonad.html] 及其来源，了解如何使用合适的示例。例如，可以定义Suitable m (Map a b)，并打印地图中的元素数量。

question

goal：现在，我有一个 monad 转换器MyMonadT，并且想要制作MyMonadT m a PrintSuitable实例每当m is a PrintSuitable实例。

2 级约束动机: 问题在于类型a介绍了关于printSuitable函数，即不会出现在class签名。由于只能对class签名（附加约束instance函数实现是非法的），说一些关于所有的事情是有道理的a在类签名中（下面第 2 行）。

下面显示了预期的代码。

instance (PrintSuitable m, MonadTrans t,
        (forall a. Suitable (t m) a => Suitable m a), -- rank 2 constraint
        ) => PrintSuitable (t m) where

    printSuitable = lift ...

-- MyMonadT doesn't change what values are Suitable, hence the rank 2 expression,
-- (forall a. Suitable (t m) a => Suitable m a) should hold true
data instance Constraints (MyMonadT m) a =
    Suitable m a => MyMonadT_Constraints
instance Suitable m a => Suitable (MyMonadT m) a where -- the important line
    constraints = MyMonadT_Constraints

instance MonadTrans MyMonadT where ...
-- now, MyMonadT m is a PrintSuitable whenever m is a PrintSuitable

-- the manual solution, without using MonadTrans, looks roughly like this
instance PrintSuitable m => PrintSuitable (t m) where
    printSuitable a = withResConstraints $ \MyMonadT_Constraints -> ...

所指示的约束表示任何适合的东西(t m)适合于m。但是，当然，这不是有效的 Haskell；如何编码一个等价的功能？

提前致谢！！！

做你要求的事

如果你看看我关于 hackage 的约束包，有

数据.约束.Forall

这可用于创建量化约束，并将 inst 与包中的其他约束组合器一起使用，并通过创建辅助约束将参数放在正确的位置，您可以直接对您所要求的内容进行编码。

我的博客上有反射机制的描述。

http://comonad.com/reader/2011/what-c​​onstraints-entail-part-1/ http://comonad.com/reader/2011/what-constraints-entail-part-1/

http://comonad.com/reader/2011/what-c​​onstraints-entail-part-2/ http://comonad.com/reader/2011/what-constraints-entail-part-2/

然而，这需要前沿的 GHC。

在许多情况下，您通常可以通过制作特定约束的等级 2 版本来模仿这一点。

class Monoid1 m where
    mappend1 :: m a -> m a -> m a
    mempty1 :: m a

但在您的情况下，您不仅需要 2 级约束，还需要约束含义。

使用该包中的机器，我们could make

class SuitableLowering t m where
   lowerSuitability :: Suitable (t m) a :- Suitable m a

然后你可以使用

instance (PrintSuitable m, SuitableLowering t m) => PrintSuitable (t m) where

and use expr \\ lowerSuitability手动将其纳入范围Suitable m a在你知道的上下文中的实例Suitable (t m) a.

但这是表达实例的一种非常危险的方式，因为它阻止您制作某种 (* -> *) -> * -> * PrintSuitable 的实例以任何其他方式如果您不小心，可能会干扰您的基本情况的定义！

做你需要做的事

The right做到这一点的方法是放弃定义涵盖所有情况的单个实例，而是定义一个printSuitableDefault可用于任何合适的变压器。

假设丹尼尔的回复中提到的 RMonadTrans 的存在

class RMonadTrans t where
    rlift :: Suitable m a => m a -> t m a

我们可以定义：

printSuitableDefault :: (RMonadTrans t, Suitable m a) => a -> t ()
printSuitableDefault = ...

instance PrintSuitable m => PrintSuitable (Foo m) where
  printSuitable = printSuitableDefault

instance PrintSuitable m => PrintSuitable (Bar m) where
  printSuitable = printsuitableDefault

您不可能有太多的 rmonad 转换器，这确保了如果您想以不同的方式进行打印，您可以拥有这种灵活性。

在前沿编译器下更好地完成您需要的事情

在 7.3.x（当前的 GHC HEAD）或更高版本中，您甚至可以使用新的默认声明来减轻这种痛苦。

class RMonad m => PrintSuitable m where
   printSuitable :: a -> m ()
   default printSuitable :: (RMonadTrans t, RMonad n, Suitable n a, m ~ t n) => 
     a -> t n ()
   printSuitable = <the default lifted definition>

那么每个变压器的实例可以看起来像：

instance PrintSuitable m => PrintSuitable (Foo m)
instance PrintSuitable m => PrintSuitable (Bar m)

你可以为一些受限的单子定义你的漂亮打印合适的基本情况，而不必担心重叠。