问题描述
这些之间的区别究竟是什么？我想我明白存在类型是如何工作的，他们就像在OO中有一个基类，而没有下沉的方法。通用类型有何不同？
这里的术语universal和existential来自。
通常写为∀，您可以阅读为for all，并且大致意味着它听起来像：在类似∀x。...的逻辑语句中，任何替代...的语句都适用于所有可能的x，您可以选择从任何一组事物量化。
，通常在Haskell中称为多态，在其他一些语言中（例如C＃ ）被称为泛型。
存在量化类型如存在a。 a - >一个意味着对于某些特定的类型a，我们可以实现一个类型为 a - >的函数。一个。任何函数都可以，所以我会选择一个：
func :: exists a。 a - > a
func True = False
func False = True
...哪当然是布尔值的不功能。但问题在于我们不能使用，因为我们所知的类型a就是它存在。任何有关 类型的信息都被丢弃了，这意味着我们不能将 func 应用于任何值。
这并不是非常有用。
那么我们可以用 func做什么 ？那么，我们知道它是一个输入和输出具有相同类型的函数，所以我们可以自行编写它。从本质上讲，你可以用具有存在类型的东西做的唯一事情是你可以根据类型的非存在性部分做的事情。同样，给定类型的东西存在a。我们可以找到它的长度，或者将它连接到它自己，或者删除一些元素，或者我们可以对任何列表进行的任何操作。
最后一点让我们回到普遍的量词，并且Haskell 没有直接存在的类型（我的存在以上完全是虚构的，唉）：因为具有存在量化类型的事物只能用于具有普遍量化类型的操作，所以我们可以写出存在的类型a。 a 作为 forall r。 （全部a - > r） - > r - 换句话说，对于所有结果类型 r ，给定一个函数，对于所有类型 a 接受一个类型为 a 的参数并返回一个类型为 r 的值，我们可以得到键入 r 。
如果您不清楚为什么它们几乎相同，请注意整体类型不是普遍量化 a - 相反，它需要一个参数，它自身被普遍量化为 a ，然后它可以使用它选择的任何特定类型。
另外，虽然Haskell并没有真正的子类型概念通常意义上说，我们可以把量词视为表达一种子类型的形式，层次从普遍到具体到存在。 类型的东西a。一个可以转换为任何其他类型，所以它可以被看作是一切的一个子类型;另一方面，任何类型都可以转换为类型 exists a。一个，使它成为一切的父类型。当然，前者是不可能的（除错误之外，没有类型的值），而后者是无用的（你不能用类型存在a。a ），但类比至少在纸上起作用。 ：]
请注意，存在型和普遍量化参数之间的等价关系与 1：不完全 - 只有当我们忽略导致错误的函数时，比如 notId x = undefined ，包括永不终止的函数，比如 loopForever x = loopForever x 。 2： GHC。好吧，GHC。没有扩展，Haskell只具有隐式通用量词，根本没有讨论存在类型的真正方法。 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. 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. 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. 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". 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: 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. 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". 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: ...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. This is not very useful. 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. 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. 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. 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. :] 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: 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: Well, GHC. Without extensions, Haskell only has the implicit universal quantifiers and no real way of talking about existential types at all. 这篇关于Haskell中的存在与量化类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！
id :: forall a. a -> a
id x = x
func :: exists a. a -> a
func True = False
func False = True