3

I have been reading the existential section on Wikibooks and this is what is stated there:

Firstly, forall really does mean 'for all'. One way of thinking about types is as sets of values with that type, for example, Bool is the set {True, False, ⊥} (remember that bottom, ⊥, is a member of every type!), Integer is the set of integers (and bottom), String is the set of all possible strings (and bottom), and so on. forall serves as an intersection over those sets. For example, forall a. a is the intersection over all types, which must be {⊥}, that is, the type (i.e. set) whose only value (i.e. element) is bottom.

How does forall serve as an intersection over those sets ?

forall in formal logic means that it can be any value from the universe of discourse. How does in Haskell it gets translated to intersection ?

4

3 回答 3

4

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都可以被视为某些产品的查找函数，其中键具有 type a，元素具有 type 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。

所以，让我们先看一下普通产品的代数。代数类型被称为代数，因为我们可以通过代数确定它们的值的数量。链接到详细解释。如果A具有|A|多个值并且B具有|B|多个值，则Pair A B具有|A| * |B|多个可能值。使用总和类型，我们将居民数量相加。由于A -> B可以看作是一个具有|A|字段的产品，所有字段都具有 type B，因此居民的A -> B数量|A|是|B|-s 的数量相乘，等于|B|^|A|. 因此，有时用于表示函数的名称“指数类型”。当函数依赖时，我们回退到“对一些不同类型的乘积”解释，因为指数公式不再适用。

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

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

于 2014-08-17T12:47:27.473 回答
3

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

在这里，您可能会受益于开始阅读有关Curry-Howard 对应关系的内容。长话短说，您可以将类型视为逻辑命题，将语言表达式视为其类型的证明，将值视为范式证明（无法进一步简化的证明）。例如，"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真环境的交集。AB

于 2014-08-18T18:20:21.803 回答
3

您必须在消极或积极的上下文中查看类型——即在构造过程或使用过程中（拥有/接收，这可能在游戏语义中得到最好的理解，但我不熟悉它们）。

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

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

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

absurd :: (forall a . a) -> b
absurd a = a
于 2014-08-16T23:14:17.327 回答