Haskell中的存在与量化types

这些差别究竟是什么? 我想我明白存在types是如何工作的,他们就像在OO中有一个基类,没有下滑的方法。 普遍types如何不同?

One Solution collect form web for “Haskell中的存在与量化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的方法。

  • 如何用printfs“debugging”Haskell?
  • 文本或字节串
  • “米尔纳 - 辛德雷的哪一部分你不明白?
  • 为什么Haskell(GHC)如此快速?
  • 如何debuggingHaskell代码?
  • 在(function)编程的背景下,“具体化”和“具体化”是什么意思?
  • 集合,函数和Eq混淆
  • 什么Haskell表示推荐用于二维,无盒子像素arrays与数百万像素?
  • 我如何使用修复程序,它是如何工作的?
  • 榆木编译器永远运行,电脑刚刚变热
  • Haskell函数可以certificate/模型检查/validation的正确性属性?