什么是类型量词？

Question

T Foo<T>(T x){ return x; }

int y = Foo<int>(3);

这些类型有时也是这样写的：

Foo :: forall T. T -> T

我曾听人说过“Forall就像Lambda--类型级别的抽象”。因此Foo是一个接受类型（例如int）并生成值的函数（例如int->int类型的函数）。许多语言都推断类型参数，这样您就可以编写foo(3)而不是foo (3) 。

假设我们有一个对象f，类型为forall t->T。对于这个对象，我们可以做的是首先通过编写f来传递一个类型q。然后返回一个类型为q->q的值。但是，某些f无效。例如，此f:

f<int> = (x => x+1)
f<T> = (x => x)

forall n in Integers: P(n)

forall n in Integers: P(n) == forall(Integers,P)

forall :: Set<T> -> (T -> bool) -> bool

Exists具有相同的类型。Forall就像一个无限连词,其中S[n]是集合S的第n个：

forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ...

Exists就像一个无限的分离：

exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ...

如果我们用类型做类比，我们可以说，∑的类型类比是计算交型Ⅶ，Ⅸ的类型类比是计算并型Ⅶ.然后我们可以在类型上定义forall和exists,如下所示：

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, exists :: Set<T> -> (T -> Type) -> Type

forall(Types, t => (t -> t))

id :: forall T:Type. T -> T
id = (x => x)

id2 = id :: int -> int

一个有类型理论知识的人能解释什么是真正存在的吗？而“Forall在类型级别上是lambda”在多大程度上是真的呢？

Answer 1

让我分别回答你们的问题。

>

将forall称为“类型级别的lambda”是不准确的，原因有两个。首先，它是lambda的类型，而不是lambda本身。第二，lambda存在于术语级别，即使它对类型进行抽象（类型级别的lambda也存在，它们提供通常称为泛型类型的东西）。

通用量化并不一定意味着所有实例都有“相同的行为”。这是一种称为“参数性”的特殊属性，它可能存在，也可能不存在。简单的多态lambda演算是参数的，因为您无法表达任何非参数行为。但是如果您添加了像typecase（也称为内涵类型分析）这样的构造，或者作为其较弱形式的checked强制转换，那么您就会放松参数性。参数性意味着良好的属性，例如，它允许在没有任何类型的运行时表示的情况下实现语言。它归纳了非常强的推理原则，参见Wadler的论文“定理免费！”。但这是一个权衡，有时你想要分派类型。

pack（Int，(x.x,x.x））：T（Int T）×（T Int）

这是一个简单的ADT，它的表示形式是Int，它只提供了两个操作（作为一个嵌套的元组），用于在抽象类型T中转换Int和从抽象类型T中转换Int。例如，这是模块类型理论的基础。

总而言之，通用量化提供了客户端数据抽象，而存在类型则双重提供了实现方数据抽象。