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

Question

如上所述这个问题/答案,Functor实例唯一确定的,如果他们存在.

对于列表,有两个众所周知的Applicative实例:[]和ZipList.因此,应用型不是唯一的(见GHC可以导出函子与应用型实例的单子变压器？而且为什么没有-XDeriveApplicative推广？).但是,ZipList需要无限列表,因为它pure无限期地重复给定元素.

• 是否有其他可能更好的数据结构示例至少有两个Applicative实例？
• 有没有这样的例子只涉及有限的数据结构？也就是说,就像假设Haskell的类型系统区分归纳和共同数据类型一样,是否有可能唯一地确定Applicative？

去进一步,如果我们能够扩大双方[]和ZipList一个单子,我们会在那里有一个单子不是唯一的数据类型和其确定的函数对象的例子.唉,只有当我们将自己限制在无限列表(流)时才有ZipList Monad实例.并且为了创建单元素列表,所以它需要有限列表.因此:return[]

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

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

• Monad实例是否由Applicative实例唯一确定,或者是否有一个Applicative的示例可以有两个不同的Monad实例？
• 是否存在具有两个不同Monad实例的数据类型的示例,每个实例具有不同的Applicative超实例？

最后我们可以为Alternative/MonadPlus提出同样的问题.由于存在两组不同的MonadPlus法则,这很复杂.假设我们接受一套法律(对于Applicative我们接受右/左分配/吸收,也参见这个问题),

• 是由Applicative唯一确定的替代品,Monad的MonadPlus,还是有反例？

如果以上任何一个都是独一无二的,我会有兴趣知道为什么,要有一丝证明.如果没有,反例.

Answer 1

首先,因为Monoids不是唯一的,所以Writer Monads或Applicatives 都不是.考虑

data M a = M Int a

然后你可以给它Applicative和Monad实例同构的任何一个:

Writer (Sum Int)
Writer (Product Int)

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

ReaderT s (Writer s)
State s

至于有一个Applicative实例扩展到两个不同的Monads,我不记得任何一个例子.然而,当我试图完全说服自己是否ZipList真的不能成为一个时Monad,我发现以下相当强烈的限制适用于任何Monad:

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

这并不给join用于所有值虽然:在列表中的情况下,限制值,其中所有的元件具有相同的长度,即,具有"矩形"形状列表的列表的那些.

(对于Readermonad,其中monadic值的"形状"不变,这些实际上都是所有的m (m x)值,所以它们都有唯一的扩展.编辑:想想它Either,Maybe并且Writer也只有"矩形" m (m x)值,所以从他们的分机Applicative来Monad也是独一无二的.)

不过,如果Applicative有两个人Monad存在,我不会感到惊讶.

对于Alternative/ MonadPlus,我不记得任何法律使用左侧的分配法,而不是左捕捉的情况下,我认为没有阻止你只是换(<|>)用flip (<|>).我不知道是否有一个不那么微不足道的变化.

附录:我突然想起我已经发现的例子Applicative有两个Monad秒.即,有限列表.通常的Monad []实例,但您可以join通过以下函数替换它(基本上使空列表"具有传染性"):

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

(唉,这些名单必须是有限的,否则null支票永远不会完成,这会破坏join . fmap return == idmonad法律.)

这与列表的矩形列表上的join/ 具有相同的值concat,因此将给出相同的值Applicative.我记得,事实证明,前两个monad法则是自动的,你只需要检查ljoin . ljoin == ljoin . fmap ljoin.

Answer 2

鉴于每个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展示了一种相当简洁的方法来处理这个问题,至少当底层仿函数是一个容器时,就意义而言雅培,阿尔滕基希和加尼.

警告:提前依赖类型!

什么是容器？如果你有依赖类型,你可以统一呈现类似容器的仿函数F,由两个组件决定

1. 一组形状,S:Set
2. 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可以采取相当多的类型hackery.但这是你可以在家里尝试的东西.你会发现容器在所有通常的多项式类型形成操作下都是关闭的,以及身份,

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-structures of G-structures-all-the-same-shape",例如,[] (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)

从输入形状计算输出形状的位置,然后通过从输入位置拾取元素来填充输出位置.

(如果你是彼得汉考克,你还有另外一个比喻正在发生什么.形状是命令;位置是响应;容器态射是设备驱动程序,单向转换命令,然后响应另一个.)

每个容器态射给你一个多态函数,但反过来也是如此.鉴于这样的m,我们可以采取

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

也就是说,我们有一个表示定理,他说,两个容器之间的每个多态函数是由这样一个给定的f,g-pair.

怎么样Applicative？我们有点迷失,建造所有这些机器.但它已经是值得的.当单子和applicatives底层函子是容器,所述多态函数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(因为没有源位置的chocie),但是因为mult,我们需要那个

multS (s0, s1) = s

我们有

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

满足适当的身份和相关性条件.如果我们切换到Hancock的解释,我们为命令定义一个monoid(跳过,分号),在选择第二个命令之前无法查看对第一个命令的响应,就像命令是一副穿孔卡片一样.我们必须能够将对组合命令的响应分解为对各个命令的单独响应.

因此,形状上的每个幺半群都为我们提供了潜在的应用结构.对于列表,形状是数字(长度),并且有很多幺半群可供选择.即使形状存在Bool,我们也有很多选择.

怎么样Monad？同时,对于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

这是不平衡的,因为我们在右边有一堆形状,而不仅仅是一个.如果我们切换到Hancock的解释,我们将为命令定义一种顺序组合,我们在第一个响应的基础上选择第二个命令,就像我们在电传打字机上进行交互一样.在几何学上,我们正在解释如何将一层树的两层融为一体.如果这种组合物是独特的,那将是非常令人惊讶的.

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

我很乐意链接到Tarmo的工作细节,但它似乎还没有上街.他实际上已经使用这个分析来枚举几个底层容器选择的所有可能的monad结构.我很期待这篇论文!

编辑.通过对另一个答案的尊重,我应该观察到,在任何地方P s = (),然后(S <| P) X ~= (S, X)和monad /应用结构彼此完全重合并且与幺半群结构相对应S.也就是说,对于编写器monad,我们只需要选择形状级操作,因为在每种情况下都只有一个值的位置.