"读者"monad

Question

好的,所以编写器monad允许你将东西写入[通常]某种容器,并在最后收回容器.在大多数实现中,"容器"实际上可以是任何幺半群.

现在,还有一个"读者"monad.这一点,你可能会认为,将提供双操作-从某种容器,一个项目在一个时间逐步阅读.实际上,这不是通常的读者monad提供的功能.(相反,它只是提供了对半全局常量的轻松访问.)

要真正写一个单子这是双重平时作家单子,我们就需要某种结构是双重的独异.

1. 有没有人知道这种双重结构可能是什么？
2. 有没有人写过这个monad？它有一个众所周知的名字吗？

Answer 1

幺半群的双重是共生的.回想一下monoid被定义为(某些同构的)

 class Monoid m where
    create :: () -> m
    combine :: (m,m) -> m

有这些法律

 combine (create (),x) = x
 combine (x,create ()) = x
 combine (combine (x,y),z) = combine (x,combine (y,z))

从而

 class Comonoid m where
    delete :: m -> ()
    split :: m -> (m,m)

需要一些标准操作

 first :: (a -> b) -> (a,c) -> (b,c)
 second :: (c -> d) -> (a,c) -> (a,d)

 idL :: ((),x) -> x
 idR :: (x,()) -> x

 assoc :: ((x,y),z) -> (x,(y,z))

有法律的

idL $ first delete $ (split x) = x
idR $ second delete $ (split x) = x
assoc $ first split (split x) = second split (split x)

由于一个原因,这个类型类看起来很怪异.它有一个实例

instance Comonoid m where
   split x = (x,x)
   delete x = ()

在Haskell中,这是唯一的例子.我们可以将读者重新定义为作者的精确对偶,但由于只有一个comonoid实例,我们得到了与标准读者类型同构的东西.

所有类型都是共生的,这就是"笛卡尔封闭范畴"中的"笛卡尔"类别."Monoidal Closed Categories"类似于CCC但没有这个属性,并且与子结构类型系统有关.线性逻辑的部分吸引力在于增加了对称性,这是一个例子.而具有子结构类型允许您定义具有更有趣属性的comonoids(支持资源管理等事情).实际上,这提供了一个框架,用于理解C++中复制构造函数和析构函数的作用(尽管由于指针的存在,C++不强制执行重要的属性).

编辑:comonoids的读者

newtype Reader r x = Reader {runReader :: r -> x}
forget :: Comonoid m => (m,a) -> a
forget = idL . first delete

instance Comonoid r => Monad (Reader r) where
   return x = Reader $ \r -> forget (r,x)
   m >>= f = \r -> let (r1,r2) = split r in runReader (f (runReader m r1)) r2

ask :: Comonoid r => Reader r r
ask = Reader id

请注意,在上面的代码中,每个变量在绑定后只使用一次(因此这些变量都将使用线性类型).monad法律证明是微不足道的,只要求共生法则起作用.因此,Reader真的是双重的Writer.

Answer 2

我不完全确定幺半群的双重性应该是什么,但是想到双重(可能是错误的)与某事物相反(仅仅是因为Comonad是Monad的双重身份,并且具有所有相同的操作但相反的方式).而不是基于它mappend,mempty我会基于:

fold :: (Foldable f, Monoid m) => f m -> m

如果我们将f专门化为一个列表,我们得到:

fold :: Monoid m => [m] -> m

在我看来,这尤其包含了所有的monoid类.

mempty == fold []
mappend x y == fold [x, y]

那么,我猜这个不同的monoid类的对偶是:

unfold :: (Comonoid m) => m -> [m]

这是很多像我看到的hackage的幺因子类在这里.

所以在此基础上,我认为你描述的'读者'单子会是供应单子.供应monad实际上是值列表的状态转换器,因此在任何时候我们都可以选择从列表中提供项目.在这种情况下,列表将是unfold.supply monad的结果

我应该强调,我不是哈斯克尔专家,也不是专家理论家.但这就是你的描述让我想到的.