haskell - 排名n约束？ （或者，monad变压器和数据适合） [英] haskell -- rank n constraints? (or, monad transformers and Data.Suitable)

问题描述

我试图写一些似乎与排名2类似的东西，而不是约束。 （或者，假设在rank 2 types的定义中将 - > 更改为 => 是有意义的;如果你想得到更好的术语，请编辑该问题）。



setup

首先， 合适 typeclass（来自 Data.Suitable ，rmonad的基础）可以用来表示可以使用的值的类型。在这个问题中，我将使用

 合适的ma 
  

表示值 a 可以用作monad m某些函数的值（特别是，如果 m 是一个DSL，那么它的值通常是 a ，其中例如

  class PrintSuitable m其中
 printSuitable ::适合的ma => a  - > m（）
  

请参阅RMonad [链接]及其来源，了解如何使用合适的示例。例如，可以定义适合的m（Map ab），并打印地图中元素的数量。

问题

目标：现在，我有一个monad变换器 MyMonadT 每当 m 是一个 c> MyMonadT m a PrintSuitable PrintSuitable 实例。

rank 2约束动机：问题在于<关于 printSuitable 函数引入了code> a ，即不会出现在 class code>签名。由于只能对 class 签名添加约束（对实例函数实现的附加约束是非法的），它使得感觉在类签名（下面的第2行）中对所有 a 进行说明。 下面显示了预期的代码。

pre code> instance（PrintSuitable m，MonadTrans t，
（forall a。Suitable（tm）a => Suitable ma）， - 等级2约束
）=> PrintSuitable（tm）其中

printSuitable = lift ...

- MyMonadT不会更改适合的值，因此排名2的表达式
- - （适用的（tm）a =>适合的ma）应该保持真实的
数据实例约束（MyMonadT m）a =
适合的ma => MyMonadT_Constraints
实例适用的m a =>合适的（MyMonadT m）a其中 - 重要行
约束= MyMonadT_Constraints

实例MonadTrans MyMonadT其中...
- 现在，MyMonadT m是一个PrintSuitable，只要m是a PrintSuitable

- 不使用MonadTrans的手动解决方案，大致类似于此
实例PrintSuitable m => PrintSuitable（t m）其中
printSuitable a = withResConstraints $ \MyMonadT_Constraints - > ...


指出的约束表示任何适合（tm） 适用于 m 。但是，当然，这是无效的Haskell;怎么能编码一个功能相当的？

在此先感谢!!!

解决方案

如果您在hackage中查看我的约束包，则有

Data.Constraint.Forall

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

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

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

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

然而，这需要blee

在许多情况下，你可以通过制定特定限制的排名2版本来实现这一点。

  class Monoid1 m其中
 mappend1 :: ma  - > m a  - > ma 
 mempty1 :: ma 
  

但是在您的情况下，您不仅需要排名2限制但有一个约束的含义。

使用该包中的机器，我们可以制作

  class SuitableLowering tm其中
 lowerSuitability ::合适（tm）a： - 合适的ma 
  

然后您可以使用

 实例（PrintSuitable m，SuitableLowering tm）=> PrintSuitable（tm）其中
  

并使用 expr \\ lowerSuitability 手动将合适的ma 实例放入您知道的上下文中的适用范围（适用于（tm）a 。

但是，这是表达实例的一种非常危险的方式，因为它会阻止您制造某种类型的东西（* - > *） - > * - > *以任何其他方式使用PrintSuitable 的实例，并且可能会干扰定义您的基本情况，如果您不小心的话！
$ b 你需要什么

正确的做法是放弃定义一个覆盖所有情况的单个实例，而是定义一个可用于任何合适变换器的 printSuitableDefault 。

假设Daniel's中提到了RMonadTrans回应

  class RMonadTrans t其中
 rlift ::适合的ma => m a  - > tma 
  

我们可以定义：

  printSuitableDefault ::（RMonadTrans t，Suitable ma）=> a  - > t（）
 printSuitableDefault = ... 
 
 instance PrintSuitable m => PrintSuitable（Foo m）其中
 printSuitable = printSuitableDefault 
 
 instance PrintSuitable m => PrintSuitable（Bar m）其中
 printSuitable = printsuitableDefault 
  

您也不太可能拥有很多rmonad变形金刚，这确保了如果你想以不同的方式打印一个打印文件，你就可以拥有这种灵活性。

流血的编译器

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

  class RMonad m => PrintSuitable m其中
 printSuitable :: a  - > m（）
 default printSuitable ::（RMonadTrans t，RMonad n，Suitable n a，m〜t n）=> 
 a  - > t n（）
 printSuitable =<默认提升定义> 
  

然后每个转换器的实例可以如下所示：

  instance PrintSuitable m => PrintSuitable（Foo m）
 instance PrintSuitable m => PrintSuitable（Bar m）
  

，您可以定义您的不错的printSuitable基本案例，重叠。

I'm trying to write something that appears to be analagous to "rank 2 types", but for constraints instead. (Or, maybe it's not correct to assume changing -> in the definition of "rank 2 types" to => is meaningful; please edit the question if you think up better terminology).

setup

First, the Suitable typeclass (from Data.Suitable, the base of rmonad) can be used to denote types of values which can be used. In this question, I'll use

Suitable m a

to denote that value a can be used as a value for some functions of the monad m (in particular, if m is a DSL, then its values are usually a which are suitable), for example

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

See the top comment for RMonad [ link ] and its source for an example of how to use Suitable. For example, one could define Suitable m (Map a b), and print the number of elements in the map.

question

goal: Now, I have a monad transformer MyMonadT, and want to make MyMonadT m a PrintSuitable instance whenever m is a PrintSuitable instance.

rank 2 constraints motivation: The issue is that the type a is introduced with regard to the printSuitable function, i.e. does not appear in the class signature. Since one can only add constraints to the class signature (additional constraints to an instance function implementation are illegal), it makes sense to say something about all a in the class signature (line 2 below).

Below shows the intended code.

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 -> ...

the constraint indicated says that anything that's suitable in (t m) is suitable in m. But, of course, this isn't valid Haskell; how could one encode a functional equivalent?

Thanks in advance!!!

解决方案

Doing what you asked for

If you look in my constraints package on hackage, there is

Data.Constraint.Forall

That can be used to create quantified constraints, and using inst with the other constraint combinators from the package and by making a helper constraint to put the argument in the right position, you can directly encode what you are asking for.

A description of the reflection machinery is on my blog.

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

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

However, this requires a bleeding edge GHC.

For many cases you can often ape this by making a rank 2 version of your particular constraint though.

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

but in your case you want not only a rank 2 constraint but a constraint implication.

Using the machinery from that package we could make

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

Then you can use

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

and use expr \\ lowerSuitability to manually bring into scope the Suitable m a instance in a context where you know Suitable (t m) a.

But this is a really dangerous way to express an instance, because it precludes you ever making something is of kind (* -> *) -> * -> * an instance of PrintSuitable in any other way and may interfere with defining your base case if you aren't careful!

Doing what you need

The right way to do this is to give up on defining a single instance that covers all cases, and instead define a printSuitableDefault that could be used for any appropriate transformer.

Assuming the existence of RMonadTrans as mentioned in Daniel's response

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

we can define:

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

You aren't likely to have too many rmonad transformers, and this ensures that if you want to make one print a different way you have that flexibility.

Doing what you need slightly more nicely under a bleeding edge compiler

Under 7.3.x (current GHC HEAD) or later you can even use the new default declarations to make this a little less painful.

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>

then the instances for each transformer can just look like:

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

and you can define your nice printSuitable base case for some retricted monad without worries about overlap.

这篇关于haskell - 排名n约束？ （或者，monad变压器和数据适合）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！