鉴于每个 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表示为由两个分量决定:
- 一组形状,S: Set
- 一组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
可以通过使用一个由两个组件特定方式构造出的容器态射来实现。
- 一个函数
f : S0 -> S1
,将输入形状映射到输出形状; - 一个函数
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
和<*>
, 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
看起来我们可能需要一个幺半群。当您检查可应用法则时,您会发现我们需要恰好一个幺半群。为容器提供应用结构,就是使用适当的位置保持操作精细化其形状上的幺半群结构。对于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中,我们只需要选择形状级别的操作,因为每种情况下值都有恰好一个位置。
NonEmptyT Maybe
(其中NonEmptyT
在我发现的任何库中都没有定义,但你可以用ListT
欺骗它,只需不使用空列表即可)。 - Ørjan Johansen