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

29

正如这个问题/答案所描述的,如果存在Functor实例,则其是唯一确定的。

对于列表,有两个众所周知的应用实例:[]ZipList。因此,Applicative不是唯一的(还请参见 GHC能为monad transformer派生出Functor和Applicative实例吗? 为什么没有-XDeriveApplicative扩展?)。但是,由于pure会无限重复给定的元素,因此ZipList需要无限列表。

  • 是否存在其他至少有两个 Applicative 实例的数据结构,或许是更好的例子?
  • 是否存在仅涉及有限数据结构的这样的例子?也就是说,如果假设 Haskell 的类型系统区分归纳和余归纳数据类型,那么能否唯一确定 Applicative?

更进一步地,如果我们可以将 []ZipList 扩展到一个 Monad,我们便有了一个例子,其中 Monad 不是由数据类型及其 Functor 唯一确定的。然而,ZipList 只有在限制自己使用无限列表)时才具有 Monad 实例。而 []return 创建一个单元素列表,因此它需要有限列表。因此:

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

如果存在具有两个或多个不同实例的示例,则会出现一个明显的问题,即它们必须/可以拥有相同的Applicative实例:

  • Monad实例是否由Applicative实例唯一确定,或者有没有一个Applicative可以有两个不同的Monad实例?
  • 是否有一个数据类型的示例,其中拥有两个不同的Monad实例,每个实例都有不同的Applicative超级实例?

最后,我们可以针对Alternative/MonadPlus提出同样的问题。这复杂化了事情,因为有两个不同的MonadPlus定律集合。假设我们接受其中一个定律集合(对于Applicative,我们接受right/left distributivity/absorption,请参见this question),

  • 是Alternative由Applicative唯一确定,而MonadPlus由Monad唯一确定,还是存在任何反例?
如果上述任何一个是独特的,我会很想知道为什么,以便有一个证明的线索。如果不是,就需要一个反例。
2个回答

27

首先,由于Monoid不是唯一的,WriterMonadApplicative也不是唯一的。考虑以下情况:

data M a = M Int a

那么你可以为它提供与以下任一种同构的ApplicativeMonad实例:

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, MaybeWriter也只有"矩形"m (m x)值,所以它们从Applicative扩展到Monad也是唯一的。

我不会感到惊讶如果存在一个具有两个MonadApplicative

对于Alternative/MonadPlus,我没有记住任何使用 Left Catch 而不是 Left Distribution定律的实例。但我认为没有阻止您将 (<|>)flip (<|>) 互换。我不知道是否有更微不足道的变化。

补充说明:我突然想起我找到过一个具有两个MonadApplicative 的例子,即有限列表。有常规的 Monad [] 实例,但您可以用以下函数替换其 join 函数(基本上使空列表成为“传染性”):

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

(遗憾的是,列表需要是有限的,否则 null 检查永远不会结束,这将破坏 join . fmap return == id 单子律。)

这与列表的列表上的 join/concat 具有相同的值,因此将提供相同的 Applicative。我记得,从那个结论中,前两个单子律是自动的,你只需要检查 ljoin . ljoin == ljoin . fmap ljoin


一个“Functor”和两个“Applicatives”的例子是列表单子:它可以是一个“ZipList”或一个常规的列表,但我不确定有没有一个“Applicative”对应多个“Monad”。 - AJF
1
糟糕。我已经投过票了,所以无法再次投票以反映您的编辑。 - dfeuer
2
两个具有相同 Applicative 的 Monad 的好例子。为了清楚起见,您的第二个结构确实是一个 Monad(它是可结合的),请考虑带有吸收元素(0 s.t. 0x = 0 = x0 对于所有 x)的半群的代数理论。在集合上自由这种结构的元素是集合元素的非空序列加上 0。因此,它们与列表一一对应(将非空序列发送到非空列表,将 0 发送到空列表)。在以这种方式传输到列表后,该结构的 Monad 就是您的新 Monad [] 实例。 - Reid Barton
1
@ReidBarton 另一种理解方式,可能与你所说的等效:我得出结论,我的单子同构于 NonEmptyT Maybe(其中 NonEmptyT 在我发现的任何库中都没有定义,但你可以用 ListT 欺骗它,只需不使用空列表即可)。 - Ørjan Johansen
是的,它们至少看起来相关。两者都与具有关联的不确定性“分叉”操作和“全局”失败操作的想法相对应(与常规Monad []的“本地”失败操作相对)。 - Reid Barton

22

鉴于每个 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来说,它的唯一确定性通常是不寻常的。就像许多集合有多种方式扩展为单子群(这两者有很远的关联)。

这个答案中,我提出了一个练习,要求找到至少四个不同的有效的非空列表Applicative实例:我不会在这里透露答案,但我会给出一个寻找方法的重要提示。

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

警告:接下来是依赖类型!

什么是容器?如果你手头有依赖类型,你可以统一地将类似于容器的函子F表示为由两个分量决定:

  1. 一组形状,S: Set
  2. 一组S指数的位置,P: S -> Set

在同构意义下,F X中的容器数据结构由某个形状s:S和某个函数e:P s -> X的依赖对给出,它告诉你每个位置上的元素。也就是说,我们定义了一个容器的扩展。

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

(顺便说一下,如果你把 -> 看作是倒序指数,那么它看起来很像一个广义的幂级数)。三角形应该让你想起树节点向侧面的形状,其中元素 s:S 标记了其顶点,而底线则代表了位置集合 Ps。我们说,如果某个函子同构于 S <| P,那么它就是一个容器。

在 Haskell 中,你可以轻松地取 S = F (),但构造 P 可能需要进行一些类型操作。但这确实是你可以在家里尝试的事情。你会发现容器在所有通常的多项式类型形成操作以及恒等操作下都是封闭的。

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

构图,即从一个外部形状和每个外部位置的内部形状创建整个形状。

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

而其他一些东西,尤其是张量,其中有一个外部形状和一个内部形状(因此“外部”和“内部”是可互换的)

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

因此,F(X)G 的意思是 "F-结构的 G-结构-都具有相同的形状",例如,[](X)[] 表示矩形列表。但我跑题了

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

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

可以通过使用一个由两个组件特定方式构造出的容器态射来实现。

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

我们的多态函数就是这样:

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

输出形状是根据输入形状计算出来的,然后通过从输入位置选取元素来填充输出位置。

(如果您是Peter Hancock,则对于正在发生的事情有一个完全不同的比喻。形状是命令;位置是响应;容器态射是设备驱动程序,将命令翻译成一种方式,然后再转换为响应。)

每个容器态射都会给你一个多态函数,但反过来也是如此。给定这样的m,我们可以取:

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

换言之,我们有一个表示定理,它说明在两个容器之间的每个多态函数都由这样的f, g对给出。

Applicative呢? 在构建所有这些机制时,我们有点迷失了方向。但是这确实是值得的。当单子和应用对象的底层函子为容器时,多态函数pure<*>, returnjoin必须由相关的容器态射可表达。

让我们首先考虑应用,使用它们的幺半群表示。我们需要

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

左到右的形状映射要求我们交付

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

看起来我们可能需要一个幺半群。当您检查可应用法则时,您会发现我们需要恰好一个幺半群。为容器提供应用结构,就是使用适当的位置保持操作精细化其形状上的幺半群结构。对于unit没有什么要做的(因为没有选择源位置),但是对于mult,我们需要确保每次

multS (s0, s1) = s

我们有

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

满足适当的身份和结合性条件。如果我们转向Hancock的解释,我们正在为命令定义一个单子(skip,分号),在其中没有办法查看第一个命令的响应,然后选择第二个,就像命令是冲孔卡片一样。我们必须能够将组合命令的响应分解为各个命令的个体响应。

因此,每个形状上的单子都给我们提供了潜在的应用结构。对于列表,形状是数字(长度),有许多单子可供选择。即使形状属于Bool,我们也有相当多的选择。

那么Monad呢?同时,对于具有M ~= S <| P的单子M。我们需要

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

首先看形状,这意味着我们需要一种有点倾斜的单子。

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

因为我们在右边得到了许多形状,而不仅仅是一个形状,所以它是不对称的。如果我们采用汉考克的解释,我们正在为命令定义一种顺序组合,在这种组合中,我们确实可以根据第一个响应来选择第二个命令,就像我们在电传机上交互一样。更几何地说,我们正在解释如何将树的两层粘合成一层。如果这样的组合是唯一的,那将是非常令人惊讶的。

同样,对于位置,我们必须以连贯的方式将单个输出位置映射为一对位置。这对于单子而言更加棘手:我们首先选择一个外部位置(响应),然后我们必须选择一个适合第一个位置(第一个响应之后选择)发现的形状(命令)的内部位置(响应)。

我很想链接到塔莫的作品以获取细节,但似乎还没有公开。他实际上已经使用这种分析方法枚举了几种基础容器的所有可能的单子结构。我期待这篇论文!

编辑。 为了向其他答案致敬,我应该观察到,当 P s = () 时,(S <| P) X ~= (S, X),单子/应用结构与monoid结构完全重合,并且在writer monads中,我们只需要选择形状级别的操作,因为每种情况下值都有恰好一个位置。


2
作为一个非 Haskell 程序员:我理解其中一些词汇,只是不明白你把它们放在了什么顺序。 - Dan
1
作为另一个答案的作者:啊!我的头! - Ørjan Johansen
3
我不确定成为Haskeller有多大帮助。对于那些无法直接在Haskell中建模的数据结构,在依赖类型系统方面的见解会让人感到困惑。也许最终它可能会变得值得一试。 - pigworker
2
作为一个 Haskell 程序员,我和你差不多。但是我对此非常着迷。 - Rein Henrichs
考虑到您的编辑,我注意到 join (fmap ...) = f <$> xs <*> ys 方程可以固定所有 join 的值(本质上所有值都是我所谓的“矩形”),除非您有多个形状,并且至少有一个形状具有两个或更多位置。这最终让我想起了我的实际反例! - Ørjan Johansen

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接