haskell - 纯粹的独特性

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 的唯一性。 ，并且确实有系统 F 的模型/扩展，其中 fmap不是唯一的。
打破参数性的一个简单示例是添加类型案例(类型上的模式匹配)，这允许您定义以下 twist它检查其参数的类型并翻转它找到的任何 bool 值:

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 的回答并不矛盾，它将关于幺半群身份唯一性的通常论点转化为幺半群仿函数的设置，但它破坏了它的方法。问题是该 View 假设您已经有一个给定的仿函数，并且单曲面结构与它兼容。特别是法律 fmap f u = pure f <*> u隐含在定义 pure 中如 \x -> fmap (const x) funit (和 (<*>) 也相应地)。如果您没有修复 fmap，那么该论点就会失效。首先，因此您没有任何可依赖的连贯性法则。