纯粹的独特性

Question

对于任何Applicative 实例，一旦写入<*>，pure 就会被唯一确定。假设您有pure1 和pure2，两者都遵守法律。那么

pure2 f <*> pure1 y = pure1 ($ y) <*> pure2 f  -- interchange for pure1
pure2 id <*> pure1 y = pure1 ($ y) <*> pure2 id -- specialize f to id
pure1 y = pure1 ($ y) <*> pure2 id  -- identity for pure2
pure1 y = fmap ($ y) (pure2 id) -- applicative/fmap law for pure1
pure1 y = pure2 ($ y) <*> pure2 id -- applicative/fmap law for pure2
pure1 y = pure2 y -- homomorphism law

但是以这种方式使用fmap 法律感觉就像在作弊。有没有办法在不诉诸参数化的情况下避免这种情况？

Answer 1

当前文档中给出的法律确实依赖于参数化来连接到fmap。

如果没有参数，我们就会失去这种联系，因为我们甚至无法证明 fmap 的唯一性，而且确实存在 fmap 不是唯一的 System F 的模型/扩展。

打破参数性的一个简单示例是添加类型案例（类型上的模式匹配），这允许您定义以下twist，它检查其参数的类型并翻转它找到的任何布尔值：

twist :: forall a. a -> a
twist @Bool     = not
twist @(a -> b) = \f -> (\x -> twist @b (f (twist @a x)))
twist @a        = id  -- default case

它具有多态身份的类型，但它是not的身份函数。

然后您可以定义以下“扭曲身份”函子，其中pure 将twist 应用于其参数：

newtype I a = I { runI :: a }

pure :: a -> I a
pure = I . twist

(<*>) :: I (a -> b) -> I a -> I b  -- The usual, no twist
(<*>) (I f) (I x) = I (f x)

twist 的一个关键属性是twist . twist = id。这允许它在组合使用pure 嵌入的值时自行抵消，从而保证the four laws of Control.Applicative。 (Proof sketch in Coq)

这个扭曲的函子也产生了fmap 的不同定义，如\u -> pure f <*> u。展开定义：

fmap :: (a -> b) -> I a -> I b
fmap f (I x) = I (twist (f (twist x)))

这与 duplode 的回答并不矛盾，它将关于幺半群身份唯一性的通常论点转换为幺半群函子的设置，但它破坏了它的方法。问题是该视图假设您已经有一个给定的函子，并且单曲面结构与它兼容。特别是，将pure 定义为\x -> fmap (const x) funit （以及(<*>) 也相应地）隐含了法律fmap f u = pure f <*> u。如果您一开始就没有修复fmap，那么这个论点就会失效，因此您没有任何可依赖的一致性法则。

Answer 2

让我们切换到 applicative 的 monoidal 函子表示：

funit :: F ()
fzip :: (F a, F b) -> F (a, b)

fzip (funit, v) ~ v
fzip (u, funit) ~ u
fzip (u, fzip (v, w)) ~ fzip (fzip (u, v), w)

如果我们将a 和b 专门化为()（并查看元组同构），定律告诉我们funit 和fzip 指定了一个幺半群。由于幺半群的身份是唯一的，funit 是唯一的。对于通常的Applicative 类，pure 然后可以恢复为...

pure a = fmap (const a) funit

... 这也是独一无二的。虽然原则上尝试将此推理扩展到至少一些非完全参数化的函子是有意义的，但这样做可能需要在很多地方做出妥协：

• () 作为对象的可用性，定义funit 并陈述幺半群函子定律；

• 用于定义 pure 的 map 函数的唯一性（另请参阅 Li-yao Xia's answer），或者，如果不这样做，则以某种方式唯一指定 fmap . const 类似物的明智方法；

• 函数类型作为对象的可用性，为了用(<*>) 来说明Aplicative 法则。