代码之家 › 专栏 › 技术社区 › dfeuer

纯粹的独特性

applicative haskell

dfeuer · 技术社区 · 3 年前

对于任何 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 这样的法律感觉像是一种欺骗。有没有一种方法可以避免这种情况,而不诉诸于参数化?

0 回复 | 直到 3 年前

Mihir Ajmera Serial 3 年前

当前文件中给出的法律确实依赖于参数性来连接 fmap .

没有参数性,我们就失去了这种联系,因为我们甚至无法证明 fmap ,并且确实存在系统F的模型/扩展,其中 fmap 不是唯一的。

打破参数化的一个简单例子是添加类型case(类型上的模式匹配),这允许您定义以下内容 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 身份功能。

然后,您可以定义以下“扭曲恒等式”functor,其中 pure 应用 扭曲 对其论点:

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 = id 。这允许它在组合使用嵌入的值时自行抵消 纯净的 ,从而保证 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的答案并不矛盾,duplode将单体恒等式唯一性的通常论点转化为单体函子的设置,但它破坏了其方法。问题是,该观点假设你已经有了一个给定的函子,并且单子结构与之兼容 fmap f u = pure f <*> u 从定义中隐含 纯净的 作为 \x -> fmap (const x) funit (以及 (<*>) 也相应地)。如果你还没解决,那场争论就不成立了 fmap 首先,所以你没有任何连贯性法则可以依靠。

duplode 3 年前

让我们切换到应用程序的单调函子表示:

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 并阐述了单调函数定律;
用于定义的映射函数的唯一性 纯净的 (另见 Li-yao Xia's answer ),或者,如果做不到这一点,则以某种方式唯一指定一个 fmap . const 模拟;
函数类型作为对象的可用性,以便说明 Aplicative 法律方面 (<*>) .