纯粹的独特性

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

让我们切换到 applicative 的幺半群函子表示：

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 class，pure 可以恢复为...

pure a = fmap (const a) funit

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

()作为对象的可用性，定义funit并陈述幺半群函子定律；
用于定义 pure 的 map 函数的唯一性（另请参阅），或者，如果失败，以某种方式唯一指定 [=23] 的明智方法=]模拟；
函数类型作为对象的可用性，为了根据 (<*>).
陈述 Aplicative 法则

Answer 2

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

没有参数化，我们就失去了这种联系，因为我们甚至无法证明 fmap 的唯一性，而且确实有 models/extensions 的系统 F，其中 fmap 不是唯一的。

打破参数化的一个简单示例是添加类型大小写（类型上的模式匹配），这允许您定义以下 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 的回答并不矛盾，后者将通常关于幺半群身份唯一性的论点转化为幺半群函子的设置，但它破坏了它的方法。问题是视图假设你已经有一个给定的函子并且幺半群结构与它兼容。特别地，法则 fmap f u = pure f <*> u 隐含于将 pure 定义为 \x -> fmap (const x) funit（并且相应地 (<*>)）。如果您一开始就没有修复 fmap，那么该论点就会失效，因此您没有任何可依赖的相干定律。

纯粹的独特性

Uniqueness of pure

haskell

applicative