当前位置: 首页 > 知识库问答 >
问题:

纯唯一性

宦宏爽
2023-03-14

对于任何applicative实例,一旦编写了<*>,就唯一地确定了pure。假设您有pure1pure2,它们都遵守法律。然后

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法则感觉像是一种欺骗。有没有一种方法可以避免这种情况而不诉诸于参数性呢?

共有2个答案

韩自怡
2023-03-14

让我们转到应用程序的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)

如果我们将aB专门化为()(并查看元组同构),则定律告诉我们funitfzip指定一个么半群。由于么半群的恒等式是唯一的,所以funit是唯一的。对于通常的applicative类,pure可以恢复为...

pure a = fmap (const a) funit

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

> 以()为对象,定义funit并陈述monoidal函子定律;

纯支持定义的map函数的唯一性(另见Li-yao Xia的回答),或者,如果不能做到这一点,则可以通过某种方式唯一指定fmap。const模拟;

函数类型作为对象的可用性,以便用(<*>)来说明applicative规律。

仲柏
2023-03-14

当前文档中给出的规则依赖于参数性来连接fmap

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

打破参数性的一个简单示例是添加type-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

它具有多态标识的类型,但它是而不是标识函数。

然后可以定义以下“扭曲标识”函式,其中puretwist应用于其参数:

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。这允许它在组合使用pure嵌入的值时与自身抵消,从而保证了control.applicative的四条定律。(Coq中的校样草图)

这个扭曲的函子还产生了fmap的不同定义,如\u->纯f<*>u。展开的定义:

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

这与Duplode的回答并不矛盾,后者将关于么半群恒等式唯一性的通常论点转化为么半群函子的设置,但它破坏了它的方法。问题是,视图假设你已经有一个给定的函子,并且monoidal结构与它兼容。特别是,将pure定义为\x->fmap(const x)funit(以及(<*>)也相应地定义),就隐含了fmap f u=pure f<*>u这一定律。如果您没有首先修复fmap,那么这个论点就会失败,因此您没有任何可依赖的一致性定律。

 类似资料:
  • 更新:应聘已终止。 —————— 上来介绍完项目,然后就让我做题,合并k个有序数组。 一开始写了个O(nk)的做法,让我继续优化,然后优化成归并的过程。 然后逆天的来了: 我用c++写的,写了:int n = nums.size(); 此处nums是vector,问我说size()返回的类型是什么,我说我忘了,平时都是这么写的,他说unsigned int,说int可能表示不了,我challeng

  • 这是我的限制: 该查询证明约束实际上不起作用: 下面是输出: 为什么唯一性没有被强制执行?

  • 问题内容: 的两个实例是否可能具有相同的值? 从理论上讲,对象是从其内存地址派生的,因此所有对象都应该是唯一的,但是如果对象在GC中移动,该怎么办? 问题答案: 给定合理的对象集合,很可能会有两个具有相同的哈希码。在最好的情况下,它成为生日问题,与数以万计的对象发生冲突。在实践中,使用相对较小的可能的哈希码池创建的对象,仅数千个对象就很容易发生冲突。 使用内存地址只是获得一个稍微随机数的一种方法。

  • 以下两者之间有区别吗: 以及: 在这两种情况下,名称是否唯一?索引唯一时意味着什么? 编辑:Postgres是唯一的约束,而索引没有回答我的问题。它考虑了FK的情况。我的问题与FK无关。我只想知道在这个例子中,这两个操作是否等价,其中不涉及FK。

  • 我有一个存储任务的表,还有一个存储该任务的有序步骤的表。步骤属于一个任务父级(因此一个任务与一个步骤具有一对多的关系),每个步骤都有一个“序号”--它是哪个步骤号。我希望序号和父任务ID是一个组合的唯一约束,因此,例如,单个任务永远不能结束两个不同的步骤设置为“Step1”,但不同的任务可以各自有自己的“Step1”。 我希望能够同时更新属于一个任务的每一步的序数,这样我就不会违反唯一约束。因此,

  • 问题内容: 就性能而言,MySQL唯一索引和非唯一索引有什么区别? 假设我要在2列的组合上创建索引,并且该组合是唯一的,但是我创建了一个非唯一的索引。这会对MySQL使用的性能或内存产生重大影响吗? 同样的问题, 主 键和 唯一 索引之间有区别吗? 问题答案: UNIQUE和PRIMARY KEY是 约束 ,而不是索引。尽管大多数数据库通过使用索引来实现这些约束。除了索引之外,约束的额外开销也微不