haskell - forall 作为这些集合的交集

Question

我一直在阅读existential section维基教科书中的内容如下:

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.

forall 如何充当这些集合的交集？

forall 在形式逻辑中意味着它可以是论域中的任何值。在 Haskell 中如何将其转换为交集？

Answer 1

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

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

-- 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 绑定(bind)类型、提升类型和类型构造函数。 ，而依赖语言可以绑定(bind)任何东西。

在文献中，相关函数称为相关产品。当它们是函数时，为什么要这样调用它们呢？事实证明，我们可以仅使用依赖函数来实现 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|可能值的数量。使用 sum 类型，我们对居民数量进行求和。自 A -> B可以被视为具有 |A| 的产品字段，全部具有类型 B ， A -> B 的居民数量是 |A|数量|B| -s 相乘，等于 |B|^|A| 。因此，有时使用“指数类型”这个名称来表示函数。当函数是相关的时，我们会回到“一定数量的不同类型的乘积”解释，因为指数公式不再适合。

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

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