haskell - 排名 n 约束？ (或者，monad 转换器和 Data.Suitable)

Question

我正在尝试写一些似乎类似于“排名 2 类型”的东西，但用于约束。 (或者，假设将“等级 2 类型”的定义中的 -> 更改为 => 是有意义的；如果您想出更好的术语，请编辑问题)。

设置

一、Suitable typeclass(来自 Data.Suitable，rmonad 的基础)可用于表示可以使用的值的类型。在这个问题中，我将使用

Suitable m a

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

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

请参阅 RMonad [ link 的顶部评论。 ] 及其来源，以获取如何使用适合的示例。例如，可以定义 Suitable m (Map a b) ，并打印 map 中的元素数量。

问题

目标:现在，我有一个单子(monad)变压器 MyMonadT ，并想做 MyMonadT m一个 PrintSuitable实例每当 m是 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。如何编码一个功能等价物？

提前致谢!!!

Answer 1

做你要求的

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

数据.约束.Forall

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

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

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

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 级约束，还需要约束含义。

使用我们可以制作的那个包装中的机器

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

然后你可以使用

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

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

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

做你需要的

正确的做法是放弃定义一个涵盖所有情况的单个实例，而是定义一个 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 转换器，这确保了如果您想以不同的方式进行打印，您就有了这种灵 active 。

在最前沿的编译器下更好地完成您需要的工作

在 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)

你可以为一些受限的 monad 定义你漂亮的 printSuitable 基本情况，而不用担心重叠。