Haskell中的存在与量化类型
这些差别究竟是什么？ 我想我明白存在类型是如何工作的，他们就像在OO中有一个基类，而没有下沉的方法。 通用类型有何不同？
这里的术语“通用”和“存在”来自谓词逻辑中类似命名的量词。
通用量化通常写成∀，你可以读作“for all”，并且大致意味着它听起来像：在一个类似于“∀x...”的逻辑语句中，无论代替“...”对于所有可能的“x”都是正确的，你可以从任何一组量化的事物中进行选择。
存在量化通常被写为∃，你可以把它看作“存在”，并且意味着在类似于“∃x...”的逻辑语句中，任何代替“...”的东西对于某些未指定的从被量化的一组事物中取出“x”。
在Haskell中，量化的东西是类型（至少忽略了某些语言扩展），我们的逻辑语句也是类型，我们认为“可以实现”而不是“真实”。
所以，一个普遍量化的类型如forall a. a -> a forall a. a -> a意味着，对于任何可能的类型“a”，我们可以实现类型为a -> a的函数。 我们确实可以：
id :: forall a. a -> a
id x = x
由于a是普遍量化的，所以我们对此一无所知，因此不能以任何方式检查论证。 所以id是这种类型唯一可能的功能（1）。
在Haskell中，通用量化是“默认” - 签名中的任何类型变量都被隐含地普遍量化，这就是为什么id的类型通常被写为a -> a 。 这也被称为参数多态，在Haskell中通常被称为“多态”，在其他一些语言中（如C＃）被称为“泛型”。
存在一种存在量化类型exists a. a -> a exists a. a -> a意味着对于某些特定的类型“a”，我们可以实现一个类型为a -> a的函数。 任何功能都可以，所以我会选择一个：
func :: exists a. a -> a
func True = False
func False = True
......这当然是布尔人的“不”功能。 但问题在于我们不能像这样使用它，因为我们所知的关于“a”的类型就是它存在。 任何关于它可能的类型的信息都已被丢弃，这意味着我们无法将func应用于任何值。
这不是很有用。
那么我们可以用func做什么？ 那么，我们知道它是一个输入和输出具有相同类型的函数，所以我们可以自行编写它。 从本质上讲，你可以用具有存在类型的东西做的唯一事情是你可以根据类型的非存在性部分做的事情。 同样，给定类型的东西exists a. [a] exists a. [a]我们可以找到它的长度，或者将它连接到它自己，或者删除一些元素，或者我们可以对任何列表进行的任何其他操作。
最后一点让我们回到普遍的量词，并且Haskell（2）直接没有存在类型的原因（我exists上面exists完全是虚构的，唉）：因为存在量化类型的东西只能用于操作有普遍量化的类型，我们可以写出类型exists a. a exists a. a作为所有forall r. (forall a. a -> r) -> r forall r. (forall a. a -> r) -> r --in换句话说，所有的结果类型r给出一个函数，用于所有类型的a需要类型的参数a和返回类型的值r我们可以得到一个r型结果。
如果你不清楚为什么它们几乎是相同的，那么请注意，整体类型并不是普遍量化a ，它需要一个论点，即它本身对a全局量化a ，然后它可以用它选择的任何特定类型。
顺便说一下，虽然Haskell在通常意义上并没有真正的子类型概念，但是我们可以将量词视为表达一种子类型的形式，层次从普遍到具体到存在。 一些类型的东西forall a. a forall a. a可以转换为任何其他类型，所以它可以被看作是一切的一个子类型; 另一方面，任何类型都可以转换为exists a. a的类型exists a. a exists a. a ，使之成为父母的一切。 当然，前者是不可能的（除了错误，没有类型forall a. a值），后者是无用的（你不能做任何类型的exists a. a ），但类比至少在纸上起作用。 ：]
请注意，存在型和普遍量化论证之间的等价关系的工作原理与方差翻转功能输入的原因相同。
所以，基本的想法大致是普遍量化的类型描述对任何类型都适用的事物，而存在类型则描述了与特定但未知的类型一起工作的事物。
1：嗯，不完全 - 只有当我们忽略导致错误的函数时，比如notId x = undefined ，包括永不终止的函数，比如loopForever x = loopForever x 。
2：那么，GHC。 没有扩展，Haskell只具有隐式的通用量词，根本没有真正讨论存在类型的方法。
链接地址: http://www.djcxy.com/p/43445.html上一篇: Existential vs. Universally quantified types in Haskell