Haskell 中存在与普遍量化的类型 [英] Existential vs. Universally quantified types in Haskell

问题描述

这些之间究竟有什么区别?我想我理解存在类型是如何工作的，它们就像在 OO 中有一个基类，没有办法进行向下转换.通用类型有何不同?

What exactly is the difference between these? I think I understand how existential types work, they are like having a base class in OO without a way to down cast. How are universal types different?

推荐答案

这里的术语普遍"和存在"来自谓词逻辑.

The terms "universal" and "existential" here come from the similarly-named quantifiers in predicate logic.

通用量化通常写成∀，可以读作for all"，大致意思是听起来像:在类似于∀x...."的逻辑语句中，任何代替..."的东西对于所有可能的x"都是正确的，您可以从被量化的任何一组事物中进行选择.

Universal quantification is normally written as ∀, which you can read as "for all", and means roughly what it sounds like: in a logical statement resembling "∀x. ..." whatever is in place of the "..." is true for all possible "x" you could choose from whatever set of things is being quantified over.

存在量化通常写成∃，可以读作存在"，意思是在一个类似于∃x...."的逻辑语句，无论什么代替..."，对于取自被量化的事物集合中的某些未指定的x"都是正确的.

Existential quantification is normally written as ∃, which you can read as "there exists", and means that in a logical statement resembling "∃x. ..." whatever is in place of the "..." is true for some unspecified "x" taken from the set of things being quantified over.

在 Haskell 中，被量化的东西是类型(至少忽略某些语言扩展)，我们的逻辑语句也是类型，我们认为可以实现"而不是真实".

In Haskell, the things being quantified over are types (ignoring certain language extensions, at least), our logical statements are also types, and instead of being "true" we think about "can be implemented".

所以，像 forall a 这样的通用量化类型.一个->a 意味着，对于任何可能的类型a"，我们都可以实现一个类型为a -> 的函数；一个.事实上，我们可以:

So, a universally quantified type like forall a. a -> a means that, for any possible type "a", we can implement a function whose type is a -> a. And indeed we can:

id :: forall a. a -> a
id x = x

由于 a 是普遍量化的，我们对此一无所知，因此无法以任何方式检查参数.所以 id 是该类型唯一可能的函数⁽¹⁾.

Since a is universally quantified we know nothing about it, and therefore cannot inspect the argument in any way. So id is the only possible function of that type⁽¹⁾.

在 Haskell 中，通用量化是默认"——签名中的任何类型变量都被隐式地通用量化，这就是为什么 id 的类型通常写为 a ->一个.这也称为 参数多态性，在 Haskell 和其他一些语言(例如 C#) 称为泛型".

In Haskell, universal quantification is the "default"--any type variables in a signature are implicitly universally quantified, which is why the type of id is normally written as just a -> a. This is also known as parametric polymorphism, often just called "polymorphism" in Haskell, and in some other languages (e.g., C#) known as "generics".

一个 existentially 量化类型，如 exists a.一个->a 的意思是，对于一些特殊的 类型a"，我们可以实现一个类型为a -> 的函数；一个.任何功能都可以，所以我会选择一个:

An existentially quantified type like exists a. a -> a means that, for some particular type "a", we can implement a function whose type is a -> a. Any function will do, so I'll pick one:

func :: exists a. a -> a
func True = False
func False = True

...这当然是布尔值的非"函数.但问题是我们不能使用它，因为我们所知道的类型a"是它的存在.任何关于它可能是哪个类型的信息都已被丢弃，这意味着我们不能将 func 应用于任何值.

...which is of course the "not" function on booleans. But the catch is that we can't use it as such, because all we know about the type "a" is that it exists. Any information about which type it might be has been discarded, which means we can't apply func to any values.

这不是很有用.

那么我们可以用func做什么呢?好吧，我们知道它是一个输入和输出类型相同的函数，所以我们可以用它自己来组合它，例如.本质上，你可以对存在类型的东西做的唯一事情是你可以基于类型的非存在部分做的事情.类似地，给定 类型的东西存在 a.[a] 我们可以找到它的长度，或者将它连接到自身，或者删除一些元素，或者我们可以对任何列表做的任何其他事情.

So what can we do with func? Well, we know that it's a function with the same type for its input and output, so we could compose it with itself, for example. Essentially, the only things you can do with something that has an existential type are the things you can do based on the non-existential parts of the type. Similarly, given something of type exists a. [a] we can find its length, or concatenate it to itself, or drop some elements, or anything else we can do to any list.

最后一点让我们回到全称量词，以及 Haskell⁽²⁾ 没有直接存在类型的原因(我上面的 exists 完全是虚构的，唉):由于存在量化类型的事物只能与具有普遍量化类型的操作一起使用，我们可以写类型 exists a.a 作为 forall r.(forall a.a -> r) ->r——换句话说，对于所有结果类型 r，给定一个函数，对于所有类型 a 都采用 a 并返回 r 类型的值，我们可以得到 r 类型的结果.

That last bit brings us back around to universal quantifiers, and the reason why Haskell⁽²⁾ doesn't have existential types directly (my exists above is entirely fictitious, alas): since things with existentially quantified types can only be used with operations that have universally quantified types, we can write the type exists a. a as forall r. (forall a. a -> r) -> r--in other words, for all result types r, given a function that for all types a takes an argument of type a and returns a value of type r, we can get a result of type r.

如果您不清楚为什么它们几乎是等价的，请注意对于 a 的整体类型没有被普遍量化——相反，它需要一个本身对于 被普遍量化的参数一个，然后它可以与它选择的任何特定类型一起使用.

If it's not clear to you why those are nearly equivalent, note that the overall type is not universally quantified for a--rather, it takes an argument that itself is universally quantified for a, which it can then use with whatever specific type it chooses.

顺便说一句，虽然 Haskell 并没有通常意义上的子类型概念，但我们可以将量词视为表达子类型的一种形式，其层次结构从普遍到具体再到存在.forall a 类型的东西.a 可以转换为任何其他类型，因此可以将其视为所有内容的子类型；另一方面，任何类型都可以转换为类型 exists a.a，使它成为一切的父类型.当然，前者是不可能的(除了错误，没有 forall a.a 类型的值)而后者是无用的(你不能对类型 exists a.a 做任何事情))，但这个类比至少在纸面上是有效的.:]

As an aside, while Haskell doesn't really have a notion of subtyping in the usual sense, we can treat quantifiers as expressing a form of subtyping, with a hierarchy going from universal to concrete to existential. Something of type forall a. a could be converted to any other type, so it could be seen as a subtype of everything; on the other hand, any type could be converted to the type exists a. a, making that a parent type of everything. Of course, the former is impossible (there are no values of type forall a. a except errors) and the latter is useless (you can't do anything with the type exists a. a), but the analogy works on paper at least. :]

请注意，存在类型和普遍量化参数之间的等价性与 variance 翻转函数输入.

Note that the equivalence between an existential type and a universally quantified argument works for the same reason that variance flips for function inputs.

因此，基本思想大致是，普遍量化的类型描述了对任何类型都适用的事物，而存在类型描述了适用于特定但未知类型的事物.

So, the basic idea is roughly that universally quantified types describe things that work the same for any type, while existential types describe things that work with a specific but unknown type.

1:嗯，不完全——只有当我们忽略导致错误的函数时，例如 notId x = undefined，包括永远不会终止的函数，例如 <代码>loopForever x = loopForever x.

1: Well, not quite--only if we ignore functions that cause errors, such as notId x = undefined, including functions which never terminate, such as loopForever x = loopForever x.

2:好吧，GHC.没有扩展，Haskell 只有隐含的全称量词，根本没有谈论存在类型的真正方式.

2: Well, GHC. Without extensions, Haskell only has the implicit universal quantifiers and no real way of talking about existential types at all.

这篇关于Haskell 中存在与普遍量化的类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！