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