问题标签 [injective-function]

根据本课程，所有构造函数（对于归纳类型）都是单射且不相交的：

...类似的原则适用于所有归纳定义的类型：所有构造函数都是单射的，并且从不同构造函数构建的值永远不会相等。对于列表，cons 构造函数是单射的，并且 nil 不同于每个非空列表。对于布尔值，true 和 false 是不相等的。

（以及inversion基于此假设的策略）

我只是想知道我们怎么知道这个假设成立？

我们怎么知道，例如，我们不能定义自然数

1）一个继任者，也许是一个像这样的“双重”构造函数：

和

2）一些plus功能，以便2可以通过构造函数的两个不同序列/路线到达一个数字，S (S O)并且D (S O)？

Coq 中确保上述情况永远不会发生的机制是什么？

PS我并不是说上面的num例子是可能的。我只是想知道是什么使它不可能。

谢谢

我对 PK 候选人的信息强度有疑问。

根据我的理解，这就是我想要分享以检查它是否正确的内容，PK 候选者必须足够强大以唯一地识别一组信息，对吗？

我开始用数学方法来研究这个问题。

如果我将 codomain 定义为由我的 SEQUENCE 生成的集合，而我的域定义为一组可由 PK 识别的数据，则说明我的 PK 候选者必须至少是内射函数是正确的。

为什么至少是内射的？因为我可以“烧掉”我的序列中的一些元素，即我的 Codomain，所以我不能确定我有 Injection 和 Surjection。

我的假设和理解正确吗？

Idris 语言教程有简单易懂的依赖类型概念示例： http ://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types

这是代码：

我决定在这个例子上花更多的时间。在函数中困扰我的sum是我需要显式地将single : Bool值传递给函数。我不想这样做，我希望编译器猜测这个布尔值应该是什么。因此，我只传递Int或传递List Int给sum函数，布尔值和参数类型之间应该存在一对一的对应关系（如果我传递一些其他类型，则不能进行类型检查）。

当然，我理解，这在一般情况下是不可能的。此类编译器技巧要求我的函数isSingleton（或任何其他类似函数）是单射的。但是对于这种情况，在我看来应该是可能的......

所以我从下一个实现开始：我只是single隐含了参数。

好吧，它并没有真正解决我的问题，因为我仍然需要以下面的方式调用这个函数：

sum {single=True} 1

但我在教程中阅读了关于auto关键字的内容。虽然我不太明白是什么auto（因为我没有找到它的描述），但我决定再修补一下我的功能：

它适用于列表！

但不适用于单一值:(

有人可以解释一下目前在这种单射函数用法中是否真的可以实现我的目标？我观看了这个关于证明某些东西是单射的短视频： https ://www.youtube.com/watch?v=7Ml8u7DFgAk

但我不明白如何在我的例子中使用这样的证明。如果这是不可能的，那么编写此类函数的最佳方法是什么？

我有以下类型系列：

这只是Const变相的功能，但 GHC 8.2.1 的注入检查器不会将其识别为注入 wrt。对其第二个论点：

如果您忽略第一种情况，它会起作用，这让我相信功能已经存在，但还没有真正成熟。

我可以用其他方式制定这个，以便 GHC 识别注入性吗？它实际上是针对这个稍微复杂一点的情况（所以arr真的被使用了）：

我经常处理单射的映射。在编程术语中，这可以表示为一个字典，其中所有值都是唯一的，当然，所有键也是唯一的。

单射映射是否具有内存高效的数据结构，具有您期望从字典中获得的所有时间复杂性属性？

例如：

Two way/reverse map中的所有解决方案似乎都需要使用或组合两组映射，重点是使在双向映射上执行操作更容易。这对于完全适合内存的小型词典来说很好，但对于大型词典来说却不是很好。

要求是存储单向双向映射与仅存储单向映射的常规字典相比，不应有额外的内存开销。

我了解字典使用哈希表，它使用关联数组数据类型。根据定义，关联数组使用唯一键实现键 -> 值映射。理论上或实际上是否有可能产生一个允许反向查找的智能单射映射？

如果不可能，我会很感激解释为什么这样的结构很难或不可能以与字典相同的效率实现。

更新

在与@rpy 讨论之后（请参阅下面的评论），有关如何使用完美的可逆哈希函数设置类似 python 字典的对象的任何信息都会很有用。但是，当然，一个可行的实现将是理想的（我已经尝试过完美）。

考虑在代码库Arrows中定义的,Domains和CoDomain类型族。agda

对程序员来说很明显，它认为Arrows (Domains func) (CoDomain func) ~ func. 但我无法curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy (CoDomain func)) undefined :: func通过 GHC 的类型检查器。那是因为 GHC 不够聪明，无法推断 和 的组合Domains是单CoDomain射的。有没有办法教 GHC 呢？我想有些情况会在IsBase谓词上分裂。

以下所有工作：

...但这不是（从 GHC-8.2 开始）：

只是没有人费心去实现这一点，还是有什么特殊原因导致关闭数据家族没有意义？我有一个数据系列，我希望保持注入性，但也有机会制作一个不相交的包罗万象的实例。现在，我认为完成这项工作的唯一方法是

我有这个公认的人为的代码块

这可以编译并正常工作。但是，如果我将最终consume''定义替换为

（注意consume而不是consume'），然后我得到一个错误

如果我们假设Id是非内射的，那么就会发生错误，因为consume可能专门针对，对于一些不是consume :: Id n (t0 Bool) -> Bar n -> t0 Bool的可折叠。我明白那么多。我的问题是：为什么实际上不是单射的。它需要两个参数：第一个参数只有一个有效值，并且在第二个参数中很明显是单射的，那么为什么 GHC 认为这是一个非单射族？t0[]Id Id

我如何编写一个可以检查哈希图是否为内射（OneOnOne）的方法？这样地图中的每个值都只有一个键。我想要它，这样它就可以通过这个测试：

是否有任何资源可以找到单射的常见 map-reduce 函数？（这些功能有名称吗？）

例如，我需要映射一个数字列表

成一个元组（总和，产品）

但是这个映射不是单射的，因为列表：

产生相同的结果。

我并不特别关心反转这些函数的“难度”，但是简单和硬可逆函数的不同来源会有所帮助。

此外，如果结果不会在范围内“爆炸”，那就太好了。例如函数：

是一个 map-reduce，也是单射的，但结果是：