我认为你已经尝试过所有有趣的可能性。我们可能定义的任何Monad m => m a -> m a
函数都不可避免地会像这样:
e :: forall m a. Monad m => m a -> m a
e u = u >>= k
where
k :: a -> m a
k = _
特别地,如果
k = return
,
e = id
。为了使
e
不是
id
,
k
必须以非平凡的方式使用
u
(例如,
k = const u
和
k = flip fmap u . const
分别对应于您的两个尝试)。在这种情况下,
u
效果将被复制,导致
e
在选择许多单子
m
时无法成为单子态射。既然如此,唯一完全多态的单子态射就是
id
。
让我们更明确地阐述这个论点。
为了清楚起见,我将暂时切换到
join
/
return
/
fmap
表示法。我们想要实现:
e :: forall m a. Monad m => m a -> m a
e u = _
我们可以用什么来填充右侧?最明显的选择是
u
。单独使用,它意味着
e = id
,这看起来并不有趣。然而,由于我们还有
join
、
return
和
fmap
,我们可以选择归纳推理,以
u
作为基本情况。假设我们有一些
v :: m a
,是用手头上的工具构建的。除了
v
本身之外,我们还有以下可能性:
join (return v)
,它是v
,因此没有告诉我们任何新信息;
join (fmap return v)
,它也是v
;以及
join (fmap (\x -> fmap (f x) w) v)
,对于某些其他根据规则构建的w :: m a
和一些f :: a -> a -> a
。(将f
的类型添加m
层,如a -> a -> m a
,并添加额外的join
以删除它们将无法得出任何结论,因为我们随后必须显示这些层的来源,而事情最终会归结为其他情况。)
唯一有趣的情况是第三种情况。此时,我将采取捷径:
join (fmap (\x -> fmap (f x) w) v)
= v >>= \x -> fmap (f x) w
= f <$> v <*> w
因此,任何非u
的右侧都可以用f <$> v <*> w
的形式表示,其中v
和w
可以是u
,也可以是这种模式的进一步迭代,最终在叶子节点处达到u
。然而,这种应用表达式有一个规范形式,通过使用applicative定律将所有(<*>)
的使用重新关联到左边来获得,在这种情况下必须像这样...
c <$> u <*> ... <*> u
在这里,省略号代表零个或多个u
,由<*>
分隔,c
是一个适当元数的a -> ... -> a -> a
函数。由于a
是完全多态的,根据参数化原理,c
必须是某个像const
一样选择其参数之一的函数。因此,任何这样的表达式都可以用(<*)
和(*>)
来重写...
u *> ... <* u
在省略号处,代表有零个或多个u
,由*>
或<*
分隔,右侧没有*>
跟着<*
。
回到开头,所有非id
候选实现必须像这样:
e u = u *> ... <* u
我们也希望e
成为一个单子态射。因此,它也必须是一个适用态射。特别地:
-- (*>) = (>>) = \u v -> u >>= \_ -> v
e (u *> v) = e u *> e v
即:
(u *> v) *> ... <* (u >* v) = (u *> ... <* u) *> (v *> ... <* v)
我们现在有一个明确的反例路径。如果我们使用应用定律将两边转换为规范形式,我们仍然会在左侧得到交错的
u
和
v
,并且在右侧所有
u
之后得到所有
v
。这意味着该属性不适用于像
IO
、
State
或
Writer
这样的单子,无论
e
中有多少
(*>)
和
(<*)
,或者哪些值由任一侧的类似于
const
的函数选择。快速演示:
GHCi> e u = u *> u <* u -- Canonical form: const const <$> u <*> u <*> u
GHCi> e (print 1 *> print 2)
1
2
1
2
1
2
GHCi> e (print 1) *> e (print 2)
1
1
1
2
2
2
e = id
,否则u
的效果将被 必然 复制?(我们还可以编写e u = do _ <- u; _ <- u; _ <- u; u
并进一步结合u
-效果。)我们如何数学描述“单子值p :: m a
具有从u :: m a
复制的多个效果?” 然后,我们如何证明重复(三倍、等等)u
-效果必然导致违反单子态射定律? - winitzkie u
的方式,即使用您描述的形式为u *> ... <* u
的某些表达式?为什么我们不能找到其他聪明而复杂的fmap
、return
和join
的组合,以便得到其他东西?同时考虑应用态射也是一个不错的选择。证明适用态射的类似属性可能比证明单子态射的类似属性更容易。(唯一适用自然的适用态射是恒等态射吗?) - winitzkijoin _
可以导致非id
的结果,而第三种情况是唯一不会导致id
或无限回归的方式。(2)关于Applicative
:非正式地说,如果你的唯一 Kleisli 箭头是return
,那么你就没有使用Monad
带来的额外能力,所以最好使用Applicative
。(3)是的,类似的属性也适用于 Applicative 映射。从规范形式开始的部分,它是自包含的,应该足以作为证明。 - duplode