什么是类型量词？

Question

许多静态类型语言都具有参数多态性。例如在 C# 中可以定义：

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<int>(3)。

假设我们有一个类型为forall T. T -> T 的对象f。我们可以对这个对象做的首先是通过编写f<Q> 将类型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 是类型级别的 lambda，那么存在什么？ （即存在量化）。由于这些原因，似乎 forall 和 exists 并不是真正的“类型级别的 lambda”。但那它们是什么？我意识到这个问题相当模糊，但是有人可以帮我解决这个问题吗？

---

可能的解释如下：

如果我们看逻辑，量词和 lambda 是两个不同的东西。一个量化表达式的例子是：

forall n in Integers: P(n)

所以有两部分需要考虑：一个用于量化的集合（例如整数）和一个谓词（例如 P）。 Forall 可以看作是一个高阶函数：

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 和存在于类型如下：

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 是一个无限的并集。他们的类型是：

forall, exists :: Set<T> -> (T -> Type) -> Type

例如多态恒等函数的类型。这里Types是所有类型的集合，->是函数的类型构造函数，=>是lambda抽象：

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

现在forall T:Type. T -> T 类型的东西是一个值，而不是从类型到值的函数。它是一个值，其类型是所有类型 T -> T 的交​​集，其中 T 涵盖所有类型。当我们使用这样一个值时，我们不必将它应用到一个类型上。相反，我们使用子类型判断：

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

id2 = id :: int -> int

这会将id 向下转换为int -> int 类型。这是有效的，因为int -> int 也出现在无限交叉点中。

我认为这很有效，它清楚地解释了 forall 是什么以及它与 lambda 有何不同，但这个模型与我在 ML、F#、C# 等语言中看到的不兼容。例如在 F#您使用id<int> 来获取整数上的标识函数，这在此模型中没有意义：id 是值上的函数，而不是返回值上的函数的类型上的函数。

---

有类型理论知识的人能解释一下究竟什么是 forall 和存在吗？ “forall 是类型级别的 lambda”在多大程度上是真的？

Answer 1

让我分别解决你的问题。

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

• 通用量化不一定意味着所有实例的“相同行为”。那是一种称为“参数性”的特定属性，可能存在也可能不存在。普通的多态 lambda 演算是参数的，因为您根本无法表达任何非参数行为。但是，如果您添加诸如 typecase（又名内涵类型分析）或检查型强制转换之类的结构作为其较弱的形式，那么您将失去参数化。参数化意味着好的属性，例如它允许在没有任何类型的运行时表示的情况下实现语言。它引发了非常强大的推理原则，例如参见瓦德勒的论文“免费定理！”。但这是一种权衡，有时您希望按类型分派。

• 存在类型本质上表示类型（所谓的见证）和术语的对，有时称为包。一种常见的查看方式是抽象数据类型的实现。这是一个简单的例子：

  pack (Int, (λx.x, λx.x em>)) : ∃ T。 (Int → T) × (T → Int)

  这是一个简单的 ADT，其表示为 Int，并且只提供两个操作（作为嵌套元组），用于将 int 转换为抽象类型 T .例如，这是模块类型理论的基础。

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

• 作为补充说明，在所谓的 lambda cube 中，forall 和 arrow 被推广到 Π 型的统一概念（其中 T1→T2 = Π(x:T1 ).T2 和 ∀AT = Π(A:*).T) 并且同样存在，并且元组可以推广到 Σ 类型（其中 T1×T2 = Σ(x:T1).T2 和 ∃AT = Σ(A :*).T)。这里，类型 *是“类型的类型”。

Answer 2

补充两个已经很出色的答案。

首先，不能说forall 是类型级别的 lambda，因为在类型级别已经存在 lambda 的概念，它与 forall 不同。它出现在 F_omega 系统中，它是具有类型级计算的 System F 的扩展，例如有助于解释 ML 模块系统（F-ing modules，作者：Andreas Rossberg、Claudio Russo 和 Derek Dreyer，2010）。

在系统 F_omega 的（语法）中，您可以编写例如：

type prod =
  lambda (a : *). lambda (b : *).
    forall (c : *). (a -> b -> c) -> c

这是“类型构造函数”prod的定义，如prod a b是产品类型(a, b)的教堂编码类型。如果在类型级别存在计算，那么如果您想确保终止类型检查，则需要对其进行控制（否则您可以定义类型(lambda t. t t) (lambda t. t t)。这是通过使用“类型级别的类型系统”来完成的, 或 kind 系统。prod 将是 kind * -> * -> *。只有 kind * 的类型可以被值所占据，更高种类的类型只能应用于类型lambda (c : k) . .... 是一个类型级别的抽象，它不能是值的类型，并且可以以 k -> ... 的任何形式存在，而 forall (c : k) . .... 对在某些类型 c : k 中具有多态性的值进行分类并且是必须是地面类*。

其次，System F 的forall 与 Martin-Löf 类型理论的 Pi 类型之间有一个重要区别。在 System F 中，多态值对所有类型都做同样的事情。作为第一个近似值，您可以说forall a . a -> a 类型的值将（隐式）将t 类型作为输入并返回t -> t 类型的值。但这表明在这个过程中可能会发生一些计算，但事实并非如此。从道德上讲，当您将 forall a. a -> a 类型的值实例化为 t -> t 类型的值时，该值不会改变。有三种（相关的）思考方式：

• System F 量化有类型擦除，你可以忘记类型，你仍然会知道程序的动态语义是什么。当我们使用 ML 类型推断将多态抽象和实例化隐含在我们的程序中时，如果您将“程序”视为将要运行的动态对象，我们并没有真正让推理引擎“填补我们程序中的漏洞”和计算。

• forall a . foo 不是“为每个类型foo 生成foo 的实例@，而是一个单一类型foo，即“在未知类型a 中通用”。

• 您可以将全称量化解释为无限合取，但有一个一致性条件，即所有合取都具有相同的结构，尤其是它们的证明都相同。

相比之下，Martin-Löf 类型理论中的 Pi 类型实际上更像是接受某物并返回某物的函数类型。这就是为什么它们不仅可以很容易地用于依赖于types，而且还可以依赖于terms（依赖类型）的原因之一。

一旦您担心这些形式理论的合理性，这就会产生非常重要的影响。 System F 是impredicative（一个forall-quantified 类型量化所有类型，包括它自己），它仍然是健全的原因是这种全称量化的统一性。虽然从程序员的角度来看，引入非参数结构是合理的（我们仍然可以在一般非参数语言中推理参数性），但它很快就会破坏底层静态推理系统的逻辑一致性。 Martin-Löf 谓词理论更容易证明正确并以正确的方式扩展。

有关 System F 的这种一致性/通用性方面的高级描述，请参阅 Fruchart 和 Longo 的 97 文章 Carnap's remarks on Impredicative Definitions and the Genericity Theorem。有关在存在非参数构造的情况下系统 F 故障的更多技术研究，请参阅 Robert Harper 和 John Mitchell (1999) 的Parametricity and variants of Girard's J operator。最后，从语言设计的角度来看，关于如何放弃 global 参数化以引入非参数结构但仍然能够在本地讨论参数化的描述，请参阅 George Neis 的 Non-Parametric Parametricity，德里克·德雷尔和安德烈亚斯·罗斯伯格，2011 年。

关于“计算抽象”和“统一抽象”之间区别的讨论已经在表示变量绑定器的大量工作中重新出现。绑定结构感觉像是一种抽象（并且可以通过 HOAS 风格的 lambda 抽象来建模），但具有统一的结构，使其更像是一个数据骨架，而不是一系列结果。这已经被大量讨论过，例如在 LF 社区中，在 Twelf 中的“代表性箭头”，在 Licata&Harper 的作品中的“正箭头”等。

最近有几个人在研究“无关性”的相关概念（lambda-abstractions，结果“不依赖”于参数），但仍然不完全清楚这与参数多态性的关系有多密切。一个例子是 Nathan Mishra-Linger 与 Tim Sheard 的作品（例如Erasure and Polymorphism in Pure Type Systems）。

Answer 3

如果 forall 是 lambda ...，那么存在什么

为什么，当然是元组！

在Martin-Löf type theory 中，有 Π 类型，对应于函数/通用量化和 Σ 类型，对应于元组/存在量化。

它们的类型与您提出的非常相似（我在这里使用Agda 表示法）：

Π : (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 参数性和 Martin-Löf 类型理论是独立的。

关于参数化，人们通常参考Philip Wadler's work。