在我们将其转换为通用类型之后，我试图更好地理解编码与使用存在类型的细微差别。简而言之，在我看来，使用存在类型比编码要容易得多，我将在下面解释这对我意味着什么。为了更好地解释这一点，让我们从逻辑中的两条规则开始

1. ∀xP(x) ⇒ ¬(∃x.¬P(x))
2. ∃xP(x) ⇒ ¬(∀x.¬P(x))

由此，我们有

1. ∀x.(P(x) ⇒ Q)
2. ∀x.(¬P(x) ⩖ Q)
3. (∀x.¬P(x)) ⩖ Q
4. (¬¬(∀x.¬P(x))) ⩖ Q
5. (¬(¬(∀x.¬P(x)))) ⩖ Q
6. (¬(∃xP(x))) ⩖ Q
7. (∃xP(x)) ⇒ Q

因此，

(∃xP(x)) ⇒ Q = ∀x.(P(x) ⇒ Q)。

换句话说，如果函数的第一个参数是存在的，我们可以将存在类型拉到左边并将其表示为通用的。这就是我所说的使用存在规则。现在，通常当人们谈论普遍类型和存在类型之间的等价性时，我们会看到

∃xP(x) = ∀y.(∀xP(x) ⇒ y) ⇒ y。

这就是我所说的存在规则的编码。为了看到这种等价性，我们有

1. ∀y.(∀xP(x) ⇒ y) ⇒ y
2. ∀y.((∃xP(x)) ⇒ y) ⇒ y
3. ∀y.¬((∃xP(x)) ⇒ y) ⩖ y
4. ∀y.¬(¬(∃xP(x)) ⩖ y) ⩖ y
5. ∀y.((∃xP(x)) ⩕ ¬y) ⩖ y
6. ∀y.((∃xP(x)) ⩖ y) ⩕ (yv ¬y)
7. ∀y.(∃xP(x)) ⩖ y
8. (∃xP(x)) ⩖ ∀yy
9. ∃xP(x)

好的，所以这条规则对我说的是，存在类型是一个函数，它接受将 P(x) 转换为 ay 然后输出 y 的程序。

现在，这就是我所说的使用存在主义和建立存在主义之间的区别的意思。假设我们想用像 OCaml 这样的语言构建一个穷人的模块，我们可以用这样的程序来做

这使用了上面的存在规则。至于类型，我们有

基本上，我们要设计一个名为 simpleProg 的函数： (∃x.mypackage(x)) ⇒ 字符串。为了做到这一点，我们改为构建一个类型为 ∀x.mypackage(x) ⇒ 字符串的函数，并使用通用编码我们的包，这在大多数函数式语言中都很简单。现在，如果我们想将 int_package 和 str_package 实际编码为存在包而不是通用包，我们使用存在规则的编码，最终得到如下代码

在这里，我们有

这基本上就是我们想要的。int 和 string 类型隐藏在包装内。然后，我们看到

这也是我们想要的。真的，我们有点想要

但是类型变量为我们解决了这个问题（或者我犯了一个可怕的错误。两者之一。）

在任何情况下，如第二个程序所示，实际从一个普遍创建一个存在主义的结构似乎真的很重，而使用存在主义的结构似乎非常简单，如第一个程序所示。基本上，这就是我所说的使用存在主义比制作存在主义要容易得多的意思。

所以，真的，我的两个问题是：

1. 如果我们只关心在函数中使用存在包，那么编码为通用类型是否比创建独立存在的包更容易？假设这是真的，这似乎是因为我们可以使用通用包（上面的 mypackage 类型）对我们的存在包进行编码。
2. 如果我们限制自己只使用存在规则和使用这些通用包，我们最终会失去什么？同样，通用包是指上面 mypackage 类型的技巧。

编辑 1

camlspotter 和 Leo White 是对的，我的类型暴露在外，包裹也乱七八糟。这是相同代码的重写且非常冗长的版本

我想我在这个过程中学到的最大的东西本质上是这种重新编码技巧颠倒了事物的构造顺序。本质上，这些包建立了一个过程，在该过程中它们接受程序，然后将该程序应用于其内部表示。通过玩这个技巧，包的内部类型被隐藏了。尽管这在理论上等同于存在类型，但就个人而言，我发现该过程不同于直接实现存在的过程，例如 Pierce 的类型和编程语言一书中所描述的存在。

直接回答我上面的问题

1. 如果您只对将包直接传递给函数感兴趣，通用包技巧很有效，并且更容易实现。它绝对不是一个存在包，但它的用途与在同一上下文中使用的真正存在包非常相似，但没有解包。类似地，我的意思是我们保留将基于不同类型的包的不同表示形式传递到函数中，然后使用这些表示形式进行通用计算的能力。
2. 我们在这些通用包中失去的是将这些包视为真正的一流成员的能力。最简单的例子是我们不能把一堆这些通用包放到一个列表中，因为它们的类型是暴露的。真正的存在包隐藏了类型，因此更容易传递更大的程序。

此外，通用包是一个可怕的词。int_package 和 str_package 是专门的，因此它们并不是真正通用的。大多数情况下，我没有更好的名字。

我很难记住量化，即我知道它们的全部含义，但有没有人有一种简单的方法来回忆哪个代表哪个？

我将举一个我正在寻找的答案的例子。

为了区分水平和垂直，取第一个字母H，字母'H'中间的线是单词所表示的方向。字母“V”有两行向上，这就是这个词的意思。

Java 文档告诉我们你可以有这个贪婪的量词：

没有提到拥有X, at MOST n times.

所以我做了一个小测试：

我希望atMost是true，因为假设下限为零是安全的。相反，我遇到了一个例外：

请注意，这不是贪婪、不情愿或占有欲的事情："X{,3}?"而且"X{,3}+"也不行。

我本可以用来"X{0,3}"实现我正在寻找的模式，但这不是我的问题。

为什么X, at MOST n timesJava 的X{,n}语法中不包含正则表达式量词？

在其他编程语言或正则表达式“风味”中如何？

这个问题出现在#haskell 的讨论中。

如果它的出现是积极的，那么将深层嵌套的 forall 提升到顶部是否总是正确的？

例如：

（其中 P、S、T 应理解为元变量）

（我们通常会写成(P(a) -> S) -> T

我知道你当然可以从一些积极的位置收集foralls，比如在最后的右边->等等。

这在经典逻辑中是有效的，所以它不是一个荒谬的想法，但总的来说它在直觉逻辑中是无效的。然而，我对量词的非正式博弈论直觉，即每个类型变量都是“由调用者选择”或“由被调用者选择”表明实际上只有两种选择，您可以将所有“由调用者选择”选项提升到顶端。除非游戏中动作的交错很重要？

有没有办法使用 C++ 模板魔法（可能使用 SFINAE 等）来实现通用和存在量化？像这样的东西：

首先，让我解释一下，这个问题既不是关于如何捕获组，也不是关于如何使用量词，这是我非常熟悉的正则表达式的两个特性。对于可能熟悉奇异引擎中不寻常语法的正则表达式爱好者来说，这更像是一个高级问题。

捕获量词

有谁知道正则表达式是否允许您捕获量词？我的意思是，与 + 和 * 等量词匹配的字符数将被计算在内，并且这个数字可以在另一个量词中再次使用。

例如，假设您想确保在这种字符串中具有相同数量的 Ls 和 Rs：LLLRRRRR

你可以想象这样的语法

其中 L 的 + 量词被捕获，并且捕获的数字在 R 的量词中被称为 {\q1}

这将有助于平衡字符串中 {@,=,-,/} 的数量，例如 @@@@ "Star Wars" ==== "1977" ---- "Science Fiction" //// "乔治卢卡斯”

与递归的关系

在某些情况下，量词捕获将优雅地取代递归，例如由相同数量的 Ls 和 Rs 框起来的一段文本，a in

这个想法在下一页的一些细节中提出：捕获的量词

它还讨论了对捕获的量词的自然扩展：量词算法，适用于您想要匹配 (3*x + 1) 之前匹配的字符数的情况。

我试图找出是否存在这样的事情。

提前感谢您的见解！！！

更新

Casimir 给出了一个绝妙的答案，展示了两种方法来验证模式的各个部分是否具有相同的长度。但是，我不想在日常工作中依赖其中任何一个。这些确实是展示出色表演技巧的技巧。在我看来，这些漂亮但复杂的方法证实了问题的前提：捕获量词（例如 + 或 *）能够匹配的字符数量的正则表达式功能将使这种平衡模式非常简单，并将语法扩展为一种令人愉悦的表达方式。

更新 2（很久以后）

我发现 .NET 有一个与我所要求的功能接近的功能。添加了一个答案来演示该功能。

我在以下示例中超时。 http://rise4fun.com/Z3/zbOcW

有什么技巧可以使这项工作（例如，通过重新制定问题或使用触发器）？

我需要一个 ruby​​ 正则表达式来创建由下划线分隔的 11 个组，但如果有超过 11 个下划线，则根本不匹配。我还需要将连续的下划线理解为“空”组。这是我到目前为止所拥有的，它无法解决 > 11 下划线问题：

这里有几个示例测试用例。

应该匹配：

lat_march 疯狂更新_付费搜索_subscription-one_google_ncaa-tournament_{adid}_p__March172014_2

但不匹配：

lat_los angeles_Paid-Search_nami-media_adn_JgYno0gS7yYjNq8OT7n_LcgTN9nt6vrmbC9qlcp__-21150_49996_7006_April22014_4

我在这个网站和java教程中阅读了很多关于java中所有格量词的问题和答案，但是男人们，我还是很困惑！我不明白！例如让我们说

根据我的理解，

在我的输入字符串中，它以 foo 结尾。但是当我收到运行程序时不匹配的声明时！这是怎么发生的，我应该怎么做仍然使用（+）量词来接收匹配？提前致谢

我似乎无法弄清楚正则表达式量词。像寻找“...”这样简单的东西对我不起作用。

这是我的模式：

我理解错了吗？表达式“X{n}”的意思是，取 X 正好 n 次？

但是像 "...." 这样的字符串工作得很好，即使它不是 3 次。