haskell - 排名n约束？(或者,monad变形金刚和Data.Suitable)

Question

我正在尝试写一些似乎与"排名2类型"类似的东西,但是对于约束而言.(或者,假设将->"等级2类型"的定义更改=>为有意义可能是不正确的;如果您想出更好的术语,请编辑问题).

建立

首先,Suitable类型类(来自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)并打印地图中的元素数量.

题

目标:现在,我有一个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上查看我的约束包,那就有了

Data.Constraint.Forall

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

反思机制的描述在我的博客上.

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

http://comonad.com/reader/2011/what-c​​onstraints-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,如Daniel的回应中所述

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)

你可以为一些受限制的monad定义你不错的printSuitable基础案例而不用担心重叠.

Answer 2

一个相关的事情是你可以定义一个实例：

{-# LANGUAGE FlexibleInstances, FlexibleContexts, 
UndecidableInstances, MultiParamTypeClasses #-}
module Foo where

import Control.Monad.Trans

class Suitable m a where
    foo :: m a -> Int

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

instance (PrintSuitable m, MonadTrans t, Suitable (t m) a) => Suitable m a where
    foo = const 5

instance (PrintSuitable m, MonadTrans t) => PrintSuitable (t m) where
    printSuitable = undefined

所以你不需要约束。这会有帮助吗？