forall 作为这些集合的交集

Posted 2023-03-28

【中文标题】forall 作为这些集合的交集

【英文标题】：forall as an intersection over those sets

【发布时间】：2014-08-16 21:12:22

【问题描述】：

我一直在阅读 Wikibooks 上的 existential section，这就是那里所说的：

首先，forall 确实意味着“为所有人”。一种思考方式 types 是具有该类型的值的集合，例如，Bool 是 设置 True, False, ⊥（记住底部，⊥，是每个 类型！），整数是整数的集合（和底部），字符串是集合 所有可能的字符串（和底部），等等。 forall 作为一个 这些集合的交集。例如，forall a。 a是所有类型的交集，必须是⊥，即唯一值（即元素）为bottom的类型（即集合）。

forall 如何作为这些集合的交集？

forall 在形式逻辑中意味着它可以是话语世界中的任何值。在 Haskell 中它是如何被翻译成交集的？

【参考方案1】：

Haskell 的forall-s 可以被视为受限的依赖函数类型，我认为这是在概念上最具启发性的方法，也最适合集合论或逻辑解释。

在依赖语言中，可以绑定函数类型中的参数值，并在返回类型中提及这些值。

-- Idris
id : (a : Type) -> (a -> a)
id _ x = x 

-- Can also leave arguments implicit (to be inferred)
id : a -> a
id x = x

-- Generally, an Idris function type has the form "(x : A) -> F x"
-- where A is a type (or kind/sort, or any level really) and F is 
-- a function of type "A -> Type" 

-- Haskell
id :: forall (a : *). (a -> a)
id x = x 

关键的区别在于 Haskell 只能使用 forall 绑定类型、提升类型和类型构造函数，而依赖语言可以绑定任何东西。

在文献中，依赖函数被称为依赖产品。当它们是函数时，为什么要这样称呼它们？事实证明，我们可以只使用依赖函数来实现 Haskell 的代数积类型。

通常，任何函数a -> b 都可以被视为某些产品的查找函数，其中键的类型为a，元素的类型为b。 Bool -> Int 可以解释为一对Int-s。这种解释对于非依赖函数来说不是很有趣，因为所有的产品字段必须是相同的类型。通过依赖函数，我们的对可以是适当的多态：

Pair : Type -> Type -> Type 
Pair a b = (index : Bool) -> (if index then a else b) 

fst : Pair a b -> a
fst pair = pair True

snd : Pair a b -> b
snd pair = pair False

setFst : c -> Pair a b -> Pair c b
setFst c pair = \index -> if index then c else pair False

setSnd : c -> Pair a b -> Pair a c
setSnd c pair = \index -> if index then pair True else c 

我们在这里恢复了对的所有基本功能。此外，使用Pair，我们可以构建任意数量的产品。

那么，如何与forall-s 的解释联系起来呢？好吧，我们可以对普通产品进行解读，并为它们建立一些直觉，然后尝试将其转移到forall-s。

所以，让我们先看一下普通产品的代数。代数类型被称为代数，因为我们可以通过代数确定它们的值的数量。 Link to detailed explanation. 如果A 具有|A| 值的数量并且B 具有|B| 的值数量，则Pair A B 具有|A| * |B| 的可能值数量。使用总和类型，我们将居民数量相加。由于A -> B 可以被视为具有|A| 字段的产品，其类型均为B，因此A -> B 的居民数量为|A| 的数量|B|-s 相乘，等于@987654346 @。因此，有时用于表示函数的名称“指数类型”。当函数依赖时，我们回退到“在一些不同类型上的乘积”解释，因为指数公式不再适合。

有了这种理解，我们可以将forall (a :: *). t 解释为具有* 类型索引和t 类型字段的产品类型，其中a 可能在t 中提及，因此字段类型可能因a 的选择而异。我们可以通过让 Haskell 为 forall 推断某些特定类型来查找字段，从而有效地将函数应用于类型参数。

请注意，考虑到 Haskell 类型的潜在数量，该产品具有与索引值一样多的字段，这里几乎是无限的。

【参考方案2】：

您必须在消极或积极的上下文中查看类型，即无论是在构建过程中，还是在使用过程中（拥有/接收，这在 Game Semantics 中可能是最好理解的，但我对它们并不熟悉）。

如果我“给你”一个类型forall a . a，那么你就知道我必须以某种方式构造它。特定构造值具有 forall a . a 类型的唯一方法是，它可以成为话语领域中“所有”类型的替代——当然，这是它们功能的交集。在理智的语言中不存在这样的价值（Void），但在 Haskell 中我们有底。

bottom :: forall a . a
bottom = let a = a in a

另一方面，如果我以某种方式神奇地获得了 forall a . a 的值并且我尝试使用它，那么我们会得到相反的效果——我可以将它视为 中的任何东西话语世界中所有类型的联合（这就是您要寻找的），因此我有

absurd :: (forall a . a) -> b
absurd a = a

【讨论】：

谢谢，所以建筑更像是所有前提的结合？

正在建设中，它的行为方式是这样的，是的。您通常可以将forall a . a 视为无限积((), Int, Bool, Char, Bool + Char, ((), Int, Bool, Char), ...)。为了构建它，您需要拥有所有这些东西，为了消除它，您只需要一个。您也可以将其视为“空”总和。我的Types of Data 帖子可能会有所帮助。

谢谢，你的帖子很有启发性。您在帖子中提到的axis of construction v. use 是什么？ （我听说过 x 和 y axix 但不是这个，谷歌搜索也没有帮助）

“轴”只是指比较点。您可以考虑两种模式的类型——under construction 和under use。粗略地说，如果您正在编写函数 (a -> b)，那么您会将 a 视为 正在使用，而 b 将视为正在建设中。这种变化就是我所说的“构建和使用轴”。

啊，啊，是的！对此感到抱歉。

【参考方案3】：

forall 如何作为这些集合的交集？

在这里，您可能会受益于开始阅读有关Curry-Howard correspondence 的一些信息。长话短说，您可以将类型视为逻辑命题，将语言表达式视为其类型的证明，将值视为范式证明（无法进一步简化的证明）。例如，"Hello world!" :: String 将被解读为“"Hello world!" 是命题 String 的证明。”

所以现在将forall a. a 视为一个命题。直观地，将其视为命题变量上的二阶量化陈述：“对于所有陈述a，a。”它基本上是在断言所有命题。这意味着如果x 是forall a. a 的证明，那么对于任何命题P，x 也是P 的证明。因此，由于forall a. a 的证明是证明任何命题的证明，那么必须遵循forall a. a 的证明必须与将每个命题映射到它的证明集时得到的相同，并且走了他们的路口。所有这些集合共有的唯一范式证明（即“值”）是底部。

另一种非正式的看待它的方式是，全称量化就像一个无限合取（∀x.P(x) 就像P(c0) ∧ P(c1) ∧ ...）。从模型理论的角度来看，合取是集合交集； A ∧ B 为真的评估环境集是A 为真的环境与B 为真的环境的交集。