Applicative/Monad实例在多大程度上是唯一确定的

如本问题/答案所述，如果存在Functor实例，则它们是唯一确定的。

对于列表，有两个众所周知的应用实例:[]和ZipList。所以应用程序不是唯一的(参见GHC可以为monad transformer派生函子和应用实例吗?)为什么没有-XDeriveApplicative扩展?)。然而，ZipList需要无限列表，因为它的pure无限地重复给定的元素。

是否有其他的，也许更好的数据结构的例子，至少有两个Applicative实例?
是否有这样的例子，只涉及有限的数据结构?也就是说，就像假设Haskell的类型系统区分归纳和共归纳数据类型一样，是否有可能唯一地确定应用程序?

进一步说，如果我们可以将[]和ZipList扩展到Monad，我们就会有一个Monad不是由数据类型及其Functor唯一决定的例子。唉，ZipList只有在我们将自己限制为无限列表(流)时才有Monad实例。return对应[]创建一个单元素列表，所以它需要有限列表。因此:

Monad实例是由数据类型唯一确定的吗?或者是否有一个数据类型可以有两个不同的Monad实例的例子?

如果一个例子有两个或多个不同的实例，一个明显的问题出现了，如果他们必须/可以有相同的应用实例:

Monad实例是由Applicative实例唯一决定的，还是有一个Applicative实例可以有两个不同的Monad实例的例子?

最后我们可以对Alternative/MonadPlus问同样的问题。由于存在两套截然不同的MonadPlus定律，这一事实使情况变得复杂。假设我们接受一组定律(对于适用性，我们接受右/左分配性/吸收性，参见这个问题)，

是由Applicative唯一确定的Alternative，而MonadPlus由Monad确定，或者有任何反例吗?

如果上面的任何一个是唯一的，我很想知道为什么，有一个证明的提示。如果不是，则给出一个反例。

首先，由于Monoids不是唯一的，因此Writer、Monad和Applicatives也不是唯一的。考虑

data M a = M Int a

则可以将Applicative和Monad实例与以下任意一个同构:

Writer (Sum Int)
Writer (Product Int)

给定s类型的Monoid实例，另一个具有不同Applicative/Monad实例的同构对是:

ReaderT s (Writer s)
State s

关于让一个Applicative实例扩展到两个不同的Monad实例，我想不起来任何例子。然而，当我试图完全说服自己ZipList是否真的不能成为Monad时，我发现以下非常强的限制适用于任何Monad:

join (fmap (x -> fmap (y -> f x y) ys) xs) = f <$> xs <*> ys

这并没有给join所有值虽然:在列表的情况下，受限制的值是那些所有元素具有相同长度的，即列表的列表与"矩形"形状。

(对于Reader的单子，单子值的"形状"没有变化，这些实际上是所有m (m x)的值，所以它们确实有唯一的扩展。编辑:仔细想想，Either,Maybe和Writer也只有"矩形"m (m x)值，所以它们从Applicative到Monad的扩展也是唯一的。

如果存在一个包含两个Monad的Applicative，我也不会感到惊讶。

对于Alternative/MonadPlus，~~我记不起任何法律~~对于使用左分布定律而不是左捕获的实例，我认为没有什么可以阻止您将(<|>)与flip (<|>)交换。我不知道是否还有更细微的变化

附录:我突然想起我曾发现过一个Applicative和两个Monad的例子。也就是有限列表。这里有通常的Monad []实例，但是您可以用以下函数替换它的join(实质上使空列表具有"传染性"):

ljoin xs
| any null xs = []
| otherwise   = concat xs

(唉，列表需要是有限的，否则null检查将永远不会完成，这将破坏join . fmap return == id单子定律。)

这与矩形列表中的join/concat具有相同的值，因此将给出相同的Applicative。我记得，原来前两个单子定律是自动的，你只需要检查ljoin . ljoin == ljoin . fmap ljoin。

假设每个Applicative都有对应的Backwards，

newtype Backwards f x = Backwards {backwards :: f x}
instance Applicative f => Applicative (Backwards f) where
pure x = Backwards (pure x)
Backwards ff <*> Backwards fs = Backwards (flip ($) <$> fs <*> ff)

这是不寻常的Applicative是唯一确定的，就像(这是非常不相关的)许多集合以多种方式扩展到monoids。

在这个答案中，我设置了为非空列表查找至少四个不同的有效Applicative实例的练习:我不会在这里破坏它，但是我会给出一个关于如何查找的大提示。

同时，在最近的一些精彩的工作中(几个月前我在暑期学校看到的)，Tarmo Uustalu展示了一种相当简洁的方法来处理这个问题，至少当底层函子是容器时，在Abbott, Altenkirch和Ghani的意义上。

警告:前面有依赖类型!

什么是容器?如果手头有依赖类型，可以统一地表示类似容器的函子F，由两个组件

决定。

一组形状，S: set
一个S索引的位置集合，P: S-> set

在同构之前，fx中的容器数据结构是由某种形状s: s和某种函数e: p s -> X的依赖对给出的，它告诉你位于每个位置的元素。也就是说，定义了容器

的扩展

(S <| P) X = (s : S) * (P s -> X)

(顺便说一下，如果你把->读成反幂，它看起来很像一个广义幂级数)。三角形应该让你想起一个侧面的树节点，元素s: s标记顶点，基线表示位置集P s。如果某个函子与某个S <| P同构，我们说它是一个容器。

在Haskell中，您可以轻松地使用S = F ()，但是构造P可能需要相当多的类型编程。但是这个你可以在家里试试。您会发现容器在所有常见的多项式类型形成操作下都是封闭的，以及恒等，

Id ~= () <|  _ -> ()

构图，整个形状是由一个外部形状和每个外部位置的内部形状组成的，

(S0 <| P0) . (S1 <| P1)  ~=  ((S0 <| P0) S1) <|  (s0, e0) -> (p0 : P0, P1 (e0 p0))

和其他一些东西，特别是张量，其中有一个外部形状和一个内部形状(所以"外部"one_answers"内部"是可以互换的)

(S0 <| P0) (X) (S1 <| P1)   =   ((S0, S1) <|  (s0, s1) -> (P0 s0, P1 s1))

使得F (X) G表示"F-structures ofG-structures-all-the- shape"，例如，[] (X) []表示矩形lists-of-lists。但我离题了

容器间的多态函数每一个多态函数

m : forall X. (S0 <| P0) X -> (S1 <| P1) X

可以通过容器态射实现，它由两个组件以一种非常特殊的方式构造。

a函数f : S0 -> S1将输入形状映射到输出形状;
一个函数g : (s0 : S0) -> P1 (f s0) -> P0 s0映射输出位置到输入位置。

我们的多态函数为

 (s0, e0) -> (f s0, e0 . g s0)

从输入形状计算输出形状，然后通过从输入位置选取元素来填充输出位置。

如果你是彼得·汉考克，你会对正在发生的事情有完全不同的比喻。形状是命令;立场是回应;容器态射是一个设备驱动程序，以一种方式翻译命令，然后响应另一种方式。

每个容器态射都给你一个多态函数，但反过来也是正确的。给定这样一个m，我们可以取

(f s, g s) = m (s, id)

也就是说，我们有一个表示定理，说明两个容器之间的每个多态函数都由这样的f,g-对给出。

Applicative呢?在建造这些机器的过程中，我们有点迷路了。但它已经值得。当单子和应用程序的底层函子是容器时，多态函数pure和<*>、return和join必须用容器态射的相关概念来表示。

让我们先看应用程序，使用它们的单轴表示。我们需要

unit : () -> (S <| P) ()
mult : forall X, Y. ((S <| P) X, (S <| P) Y) -> (S <| P) (X, Y)

形状的从左到右映射要求我们传递

unitS : () -> S
multS : (S, S) -> S

所以看起来我们可能需要一个单oid。当你检查应用定律时，你会发现我们需要正好是一个单oid。给容器配上适用的结构就是在容器的形状上通过合适的定位操作来细化单调结构。对于unit没有什么可做的(因为没有选择源位置)，但是对于mult，无论何时

，我们都需要这样做。

multS (s0, s1) = s

我们

multP (s0, s1) : P s -> (P s0, P s1)

满足适当的恒等式和结合性条件。如果我们切换到汉考克的解释，我们为命令定义了一个单oid(跳过，分号)，在选择第二个命令之前，没有办法查看对第一个命令的响应，就像命令是一副打孔卡一样。我们必须能够将对组合命令的响应分解为对单个命令的单个响应。

因此，形状上的每个单oid都给了我们一个潜在的应用结构。对于列表，形状是数字(长度)，并且有许多monoids可供选择。即使形状存在于Bool中，我们也有很多选择。

Monad呢?同时，对于M和M ~= S <| P的单子。我们需要

return : Id -> M
join   : M . M -> M

首先看形状，这意味着我们需要一种不平衡的单峰。

return_f : () -> S
join_f   : (S <| P) S -> S  --  (s : S, P s -> S) -> S

它是不平衡的，因为我们在右边有一堆形状，而不是一个。如果我们切换到汉考克的解释，我们定义了一种命令的顺序组合，我们让第二个命令在第一个反应的基础上被选择，就像我们在电传打字机上互动一样。从几何上讲，我们将解释如何将树的两层融合成一层。如果这样的作品是独一无二的，那将是非常令人惊讶的。

对于位置，我们必须以连贯的方式将单个输出位置映射到成对。这对于单子来说更棘手:我们首先选择一个外部位置(响应)，然后我们必须选择一个适合于在第一个位置(在第一个响应之后选择)找到的形状(命令)的内部位置(响应)。

我很想链接到Tarmo的工作以了解细节，但它似乎还没有达到街头。实际上，他已经使用这种分析列举了几种底层容器选择的所有可能的单子结构。我很期待那篇论文!

编辑。为了尊重另一个答案，我应该注意到，当P s = (),(S <| P) X ~= (S, X)和单子/应用结构无处不在时，它们彼此完全一致，并且与S的单子结构完全一致。也就是说，对于写入器单子，我们只需要选择形状级操作，因为在每种情况下，值都只有一个位置。

相关内容

最新更新

热门标签：