haskell --秩n约束?(或,单子变换和数据,适用)

nwlqm0z1  于 2022-11-14  发布在  其他
关注(0)|答案(3)|浏览(158)

我试图写一些看起来类似于“秩2类型”的东西,但是要针对约束。(或者,假设将“秩2类型”定义中的->改为=>是有意义的,这可能是不正确的;如果你想出更好的术语,请修改问题)。
安装程序
首先,Suitable类型类(来自Data.Suitable,rmonad的基类)可以用来表示可以使用的值的类型。

Suitable m a

为了表示值a可以用作单子m的一些函数的值(特别地,如果m是DSL,则其值通常是合适的a),例如

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

查看RMonad [link]的注解和它的源代码,了解如何使用Suitable。例如,可以定义Suitable m (Map a b),并打印Map中的元素数。

个问题

  • 目标 *:现在,我有了一个单子转换器MyMonadT,只要m是一个PrintSuitable示例,我就想让MyMonadT m成为一个PrintSuitable示例。
  • 秩2约束动机 *:问题在于类型a是相对于printSuitable函数引入的,即没有出现在class签名中。(对instance函数实现的附加约束是非法的),在类签名(下面的第2行)中描述所有a是有意义的。

下面显示了预期的代码。

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中也是合适的。如何对功能等价物进行编码?
提前感谢!!!

fwzugrvs

fwzugrvs1#

"做你要求的事"
如果你看一下我的hackage约束包,
Data.Constraint.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 (t m) a的上下文中手动将Suitable 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转换器,这确保了如果你想以不同的方式打印,你有灵活性。

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

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

且您可以为一些受限单子定义合适的printSuitable基本情况,而不用担心重叠。

alen0pnh

alen0pnh2#

我认为MonadTrans在这里没有用,因为lift要求mMonad

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

instance (RMonadTrans t, Suitable m a) => Suitable (t m) a where
    constraints = ???
sqserrrh

sqserrrh3#

相关的一点是,您可以定义一个示例:

{-# 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

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

相关问题