许多静态类型语言具有参数多态性。 例如，在C＃可以定义：
T Foo<T>(T x){ return x; }
在通话的网站，你可以这样做：
int y = Foo<int>(3);
这些类型有时也这样写的：
Foo :: forall T. T -> T
我听到有人说“FORALL就像是在类型级别拉姆达抽象”。 所以foo是，需要一个类型（例如INT），并产生一个值（例如int类型的函数 - > INT）的功能。 许多语言推断类型参数，这样就可以写Foo(3)而不是Foo<int>(3)
假设我们有一个对象f类型forall T. T -> T 。 我们可以用这个对象做的是先通过它一个类型Q写f<Q> 然后我们回来与类型的值Q -> Q 。 然而，某些f的是无效的。 例如，这f ：
f<int> = (x => x+1)
f<T> = (x => x)
因此，如果我们“称之为” f<int>然后我们回来与类型的值int -> int ，一般来说，如果我们“称之为” f<Q>然后我们回去与类型的值Q -> Q ，所以这是好。 但是，一般的理解是这f类型不是有效的事情forall T. T -> T ，因为它的东西不同，这取决于哪种类型传递。 FORALL的想法是，这是明确不允许的。 另外，如果是FORALL为拉姆达类型的水平，那么什么是存在？ （即存在量化）。 由于这些原因似乎FORALL和存在是不是真的“在类型级别拉姆达”。 但他们又是什么？ 我意识到这个问题是比较模糊的，但有人可以清除此为我？
一种可能的解释如下：
如果我们看一下逻辑，量词和lambda是两回事。 量化表达的一个例子是：
forall n in Integers: P(n)
因此，有两个部分FORALL：一组量化的（如整数），和一个谓语（如P）。 FORALL可以被看作是一个高阶函数：
forall n in Integers: P(n) == forall(Integers,P)
随着类型：
forall :: Set<T> -> (T -> bool) -> bool
存在具有相同类型。 forall的是像一个无限结合，其中S [n]是第n个的Elemen到集合S的：
forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ...
存在就像是一个无限的脱节：
exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ...
如果我们做类型打个比方，我们可以说，∧的类型类似物计算的交集∩型，和∨计算联合类型∪类型的模拟。 然后，我们可以定义FORALL和存在的类型如下：
forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ... exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ...
所以FORALL是一个无限的交集和存在是一个无限的工会。 他们的类型是：
forall, exists :: Set<T> -> (T -> Type) -> Type
例如，多态同一性功能的类型。 这里Types是该组的所有类型的，和->是用于功能类型构造和=>是λ-抽象：
forall(Types, t => (t -> t))
现在类型的东西forall T:Type. T -> T forall T:Type. T -> T是一个值 ，而不是从类型值的函数。 这是一个值，其类型为所有类型T的交叉点 - >其中T范围为在所有类型。 当我们用这样一个值，我们没有将它应用到一个类型。 相反，我们使用一种亚型的判断：
id :: forall T:Type. T -> T id = (x => x) id2 = id :: int -> int
这种向下转换id有型int -> int 。 这是有效的，因为int -> int也出现在了无限的交集。
这工作出很好，我认为，它清楚地解释了FORALL是什么以及它是如何从拉姆达不同，但这种模式是什么，我像ML，F＃，C＃等。例如在F＃你做语言已经看到不兼容的id<int>获取上整数标识功能，这没有任何意义在这个模型中：ID是值的函数，而不是返回值上的函数类型上的函数。
有人用型理论知识能解释一下到底是FORALL和存在？ 到什么程度，这是真的“FORALL是拉姆达在类型级别”？
说几句话补充两个已优异的答案。
首先，一个不能说forall是在类型级拉姆达因为已经有在类型级别拉姆达的概念，它不同于forall 。 它出现在系统F_omega，的系统F的延伸与类型级计算，即有用解释ML模块的系统，例如（ F-荷兰国际集团的模块 ，由Andreas Rossberg，克劳迪奥拉索和Derek德雷尔，2010）。
（适用于语法）系统F_omega比如，你可以写：
type prod =
lambda (a : *). lambda (b : *).
forall (c : *). (a -> b -> c) -> c
这是在“类型构造”的定义prod ，如prod ab是教会编码的产品类型的类型(a, b) 如果在类型级别的计算，那么你需要控制它，如果你想确保类型检查（否则，您可以定义类型的终端(lambda t. tt) (lambda t. tt)这是通过使用完成，或者说是一种系统中的“在类型级别类型系统” prod将是一种* -> * -> *只有在那种类型*可以通过值有人居住，类型在较高的实物只能在施加。该类型电平lambda (c : k) . ....是一种类型的级抽象，不能是值的类型，并且可以住在任何一种形式的k -> ... ，而forall (c : k) . ....分类是在某种类型的多态值c : k和必然地种* 。
其次，有一个重要区别forall的系统F和丕类型马丁- LOF型理论。 在系统F，多态值做对所有类型的同样的事情 。 作为第一个近似值，你可以说，一个类型的值forall a . a -> a forall a . a -> a的旨意（隐含地）采取型t作为输入，并返回的类型的值t -> t 。 但是，这表明可能有一些计算的过程中，这是不是这种情况发生。 从道义上，当实例类型的值forall a. a -> a forall a. a -> a成的类型的值t -> t ，该值不变化。 有三个（相关）的方式来思考一下：
系统F定量有类型擦除，你可以忘掉的类型，你仍然会知道程序的动态语义是什么。 当我们使用ML类型推断离开多态性抽象和实例化隐含在我们的节目，我们并不真正让推理机“填补了我国在程序漏洞”，如果你认为“方案”作为将要运行的动态对象和计算。
一个forall a . foo forall a . foo是不是一个东西，“产生的一个实例foo每种类型的a ，但单一的类型foo是‘在一个未知类型的通用a ’。
你可以解释全称量化为无限相结合，但所有的合取具有相同结构的均匀状态，特别是他们的证明都是相似的。
相比之下，PI-类型马丁 - LOF型理论是真的更像是拿东西，返回一些函数类型。 这就是为什么他们可以很容易地使用不仅取决于类型 ，但也依赖于条件 （取决于类型）的原因之一。
一旦你关注那些正规理论的合理性这具有非常重要的意义。 系统F是impredicative（一FORALL量化的量化类型对所有类型，包括自己），为什么它仍然健全的原因是通用的量化这种一致性。 同时引入非参数构造是从一个程序员的角度合理的（我们仍然可以推理在通常-非参数语言parametricity），它很快就破坏了底层的静态推理系统的逻辑一致性。 马丁- LOF 表语理论要简单得多，证明正确并以正确的方式扩展。
对于系统F这种均匀性/通用性方面的高层次的描述，请参阅Fruchart和隆戈的97条卡尔纳普对Impredicative定义和泛型定理的言论 。 对于系统F失败的非参数构造的存在更多的技术研究，请参见Parametricity和吉拉德的歼运营商的变体由罗伯特·哈珀，约翰·米切尔（1999年）。 最后，对于描述，从语言设计的角度，就如何放弃全球 parametricity引进非参数构造，但仍然能够在当地讨论parametricity，看到非参数Parametricity由乔治·奈瑟球菌，德里克·德雷尔和Andreas Rossberg， 2011。
“计算抽象”和“统一抽象”之间的区别的这个讨论已经由代表变量粘合剂的大量工作的恢复。 绑定建筑感觉像一个抽象（并且可以通过在高阶像差风格拉姆达抽象建模），但有一个统一的结构，使得它有点像比家庭结果的数据骨架。 这已经被广泛讨论，例如在LF社区，“具象箭”在Twelf，“积极的箭头”利卡塔与哈珀的工作，等等。
最近有几个人的“无关”（λ-抽象其中结果“不依赖”的说法）的相关概念工作，但它仍然是不完全清楚这是怎么密切相关的参数多态性。 一个例子是内森·米什拉，灵儿与蒂姆·谢尔德（如工作擦除和多态性的纯类型系统 ）。
如果FORALL是拉姆达...，那么什么是存在的
为什么呢，当然是元组！
在马丁- LOF型理论 ，你有Π类型，对应功能/通用量化和Σ-类型，对应的元组/存在量化。
它们的类型非常相似，你提出了什么（我用阿格达这里符号）：
Π : (A : Set) -> (A -> Set) -> Set
Σ : (A : Set) -> (A -> Set) -> Set
事实上，Π是一个无限的产品和Σ是无限的总和。 请注意，他们不是“交叉点”和“联盟”不过，因为你提出的，因为你不能做，没有额外定义在类型相交。 （其中一种类型的值对应于其中其它类型的值）
从这两个类型构造器，你可以有一切正常，多态和相关的功能，正常和依赖的元组，以及存在性和普遍量化的语句：
-- Normal function, corresponding to "Integer -> Integer" in Haskell
factorial : Π ℕ (λ _ → ℕ)
-- Polymorphic function corresponding to "forall a . a -> a"
id : Π Set (λ A -> Π A (λ _ → A))
-- A universally-quantified logical statement: all natural numbers n are equal to themselves
refl : Π ℕ (λ n → n ≡ n)
-- (Integer, Integer)
twoNats : Σ ℕ (λ _ → ℕ)
-- exists a. Show a => a
someShowable : Σ Set (λ A → Σ A (λ _ → Showable A))
-- There are prime numbers
aPrime : Σ ℕ IsPrime
然而，这并不能在所有和AFAIK parametricity和马丁 - LOF型理论是独立的解决parametricity。
对于parametricity，人们通常所说的菲利普·沃德勒的工作 。
