类型量词是什么？

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，那么exists是什么？（即存在量化）。出于这些原因，似乎forall和exists并不真正是“类型级别的lambda”。但是它们到底是什么呢？我意识到这个问题相当模糊，但有人能为我澄清一下吗？

A possible explanation is the following:

If we look at logic, quantifiers and lambda are two different things. An example of a quantified expression is:

forall n in Integers: P(n)

So there are two parts to forall: a set to quantify over (e.g. Integers), and a predicate (e.g. P). Forall can be viewed as a higher order function:

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

With type:

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

Exists has the same type. Forall is like an infinite conjunction, where S[n] is the n-th elemen to of the set S:

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

Exists is like an infinite disjunction:

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

If we do an analogy with types, we could say that the type analogue of ∧ is computing the intersection type ∩, and the type analogue of ∨ computing the union type ∪. We could then define forall and exists on types as follows:

forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ...
exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ...

So forall is an infinite intersection, and exists is an infinite union. Their types would be:

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

For example the type of the polymorphic identity function. Here Types is the set of all types, and -> is the type constructor for functions and => is lambda abstraction:

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

Now a thing of type forall T:Type. T -> T is a value, not a function from types to values. It is a value whose type is the intersection of all types T -> T where T ranges over all types. When we use such a value, we do not have to apply it to a type. Instead, we use a subtype judgement:

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

id2 = id :: int -> int

This downcasts id to have type int -> int. This is valid because int -> int also appears in the infinite intersection.

This works out nicely I think, and it clearly explains what forall is and how it is different from lambda, but this model is incompatible with what I have seen in languages like ML, F#, C#, etc. For example in F# you do id<int> to get the identity function on ints, which does not make sense in this model: id is a function on values, not a function on types that returns a function on values.

有了类型理论的知识，有人能解释一下forall和exists具体是什么吗？并且在多大程度上可以说“forall在类型层面上就像是lambda”？

- Jules

---

如果你对这种东西感兴趣，你应该会对《类型与编程语言》(http://www.cis.upenn.edu/~bcpierce/tapl/)非常感兴趣。 - Dan Burton

Answer 1

让我分别回答你的问题。

- 称呼forall为“类型级别的lambda”是不准确的，有两个原因。首先，它是一个lambda的类型，而不是lambda本身。其次，该lambda存在于项级别，尽管它抽象出了类型（类型级别的lambda也存在，它们提供通常称为泛型类型的内容）。 - 普遍量化并不一定意味着所有实例具有相同的行为。这是一个称为“参数性”的特定属性，可能存在也可能不存在。纯多态lambda演算是参数的，因为你根本无法表达任何非参数性的行为。但是，如果你添加像typecase（也称为内涵类型分析）或作为弱形式的检查转换这样的结构，那么你就会丧失参数性。参数性意味着很好的属性，例如它允许一种语言在没有任何类型运行时表示的情况下被实现。它还引发了非常强的推理原则，例如Wadler的论文“Theorems for free!”。但这是一个权衡，有时候你需要根据类型进行调度。 - 存在性类型本质上表示一种类型（所谓的证人）和一个术语的对，有时称为包裹。一种常见的视图是将它们看作是抽象数据类型的实现。下面是一个简单的例子： pack (Int, (λx. x，λx. x))：∃T。(Int→T)×(T→Int) 这是一个简单的ADT，其表示形式为Int，并且只提供两个操作（作为嵌套元组），用于将Int从抽象类型T转换出来。这是模块类型理论的基础，例如。 - 总之，全称量化提供了客户端数据抽象，而存在性类型双重提供了实现者数据抽象。 - 作为补充说明，在所谓的lambda立方体中，forall和arrow被推广到Π类型的统一概念上（其中T1→T2 = Π(x:T1).T2并且∀A.T = Π(A:*).T），同样的存在性和tupling可以推广到Σ类型上（其中T1×T2 = Σ(x:T1).T2并且∃A.T = Σ(A:*).T）。在这里，类型*是“类型的类型”。

- Andreas Rossberg

---

因此，类型为forall T.Q的值是类型为*->Q的函数，原则上它可以是任何这样的函数，只是有些语言只允许您表达某个符合参数性质的子集？我在“可能的解释...”中描述的模型无效，或者至少在类型理论中没有使用？Π和Σ似乎与我在那里描述的forall和exists非常相似，只是它们执行产品和标记联合而不是联合和交集？ - Jules

谢谢你的帮助。你在非参数参数性方面的工作特别有帮助。我仍在消化所有这些信息。你有书推荐吗？我有《类型与编程语言实现》（TAPL），但它并没有详细解释所有这些事情。 - Jules

不用客气。很遗憾，除了TAPL之外，我不知道有哪些像样的书籍详细讨论这个问题。在那种情况下，您可能需要查看实际的研究论文。您具体在寻找什么？ - Andreas Rossberg

普遍量化提供客户端数据抽象 - 为什么您提到数据？我们不是在从类型中进行抽象吗？否则，这是非常有教育意义的答案。感谢您分享您的知识！ - user6445533

@ftor，"数据抽象"就像抽象的数据类型一样。你说得对，它是在抽象化类型，但同时也包括相关数据的表示方式，这也是这个术语的来源。 - Andreas Rossberg

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)的 Church 编码类型。如果在类型层面上进行计算，则需要控制它以确保类型检查的终止（否则可以定义类型(lambda t. t t) (lambda t. t t)）。这可以通过使用“类型层次结构”或kind系统来实现。 prod 的 kind 是 * -> * -> *。只有 kind 为 * 的类型才能被值所占据，高级 kind 的类型只能在类型层面上应用。 lambda (c : k) . .... 是一种不能成为值类型的类型层面抽象，可以存在于任何形式为 k -> ... 的 kind 中，而 forall (c : k) . .... 则分类为多态的值类型，其中某些类型 c : k 是必须的，并且必须是 ground kind *。

其次，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不是“为每种类型a生成foo的实例的东西，而是一个在未知类型a中“通用”的单个类型foo。”

• 您可以将普遍量化解释为无限连词，但有一个一致性条件，即所有连词都具有相同的结构，并且特别是它们的证明都是相似的。

相比之下，在Martin-Löf类型论中的Pi类型更像是接受某些内容并返回某些内容的函数类型。这就是它们可以轻松地不仅依赖于类型，而且还依赖于术语（依赖类型）的原因之一。

这对于关注形式理论的可靠性非常重要。System F是不可预测的（forall-量化类型量化所有类型，包括它自己），而它仍然保持正确性的原因是普遍量化的一致性。虽然从程序员的角度引入非参数构造是合理的（我们仍然可以推断出一个通常非参数的语言的参数性），但它很快破坏了底层静态推理系统的逻辑一致性。Martin-Löf的可预测理论在正确证明和正确扩展方面要简单得多。

关于System F的统一性/通用性方面的高级描述，请参阅Fruchart和Longo的97篇文章Carnap's remarks on Impredicative Definitions and the Genericity Theorem。有关在存在非参数构造时System F失败的更多技术研究，请参阅Robert Harper和John Mitchell（1999）的Parametricity and variants of Girard's J operator。最后，关于如何放弃全局参数性并引入非参数构造但仍能在本地讨论参数性的语言设计观点的描述，请参阅George Neis、Derek Dreyer和Andreas Rossberg的2011年作品Non-Parametric Parametricity。

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

最近，有几个人正在研究与“无关性”的相关概念（即结果“不取决于”参数的 lambda 抽象），但目前还不清楚这与参数多态性的密切程度。其中一个例子是 Nathan Mishra-Linger 与 Tim Sheard 的工作（例如 Erasure and Polymorphism in Pure Type Systems）。

- gasche

---

是的！这正是我的意思。在机器学习中，类型 forall a. a -> a 意味着有一个单一值，它既具有类型 int -> int，也具有类型 string -> string 等等。这让我感到困惑，并且仍然觉得将其建模为接受类型并每次返回相同值的函数有点不妥。唯一保证它是相同值的事情是 ML 中某些特定功能的缺失。有一种明确的方式来表达“这个单一值具有所有类型 a -> a”，这似乎更加清晰（例如，当 a 范围涵盖类型时，a -> a 的交集）。但是这种方式不存在吗？ - Jules

我对System F本身毫不怀疑，因为我看到没有任何构造依赖于类型。然而，并不总是希望所有东西都具有参数化性。编写一些依赖于类型参数的代码通常很有用。另一方面，您不希望失去诸如id、map等函数的参数化性。 我想我的问题是：如何同时兼顾参数化和参数化性？其中一部分是：如果像id这样的函数不依赖于类型，那么它为什么首先是该类型的函数呢？ - Jules

一部分的动机并不来自于类型，而是来自于契约。值可以很容易地通过契约进行参数化，因为契约本身就是值。然而，如果你这样写 id：id c x = x，并且你将依赖性契约 (c:Contract) -> (c -> c) 应用于它以确保它的行为正确，那么这并不能给你带来参数性。与其依赖于语言无法根据类型/契约进行分派，需要一些其他的构造来让你明确地说出“我想要在这里使用参数性”。有一篇关于参数契约的论文，但同样不喜欢它的原因也适用。 - Jules

关于合约，我认为你仍然希望它们不会影响它们所保护的计算。你需要正式化“合约可擦除性”的概念，并表明没有任何合约会影响返回的结果（除了导致合约失败，这与所有其他计算结果都不同）。如果c具有合约类型，则不应允许使用choose c x y = if c x then x else y。这不仅是对类型系统的看法，也是对你的语言设计的看法。现在你可以使用类型系统特性来控制合约的可擦除性，但我声称你总是想要它。 - gasche

所以我认为关于参数化合约仍有待发现的地方。感谢您的帮助。您提供的链接非常有用，特别是Andreas在非参数化参数性方面的工作，因为类似的封闭机制可以应用于合约。 - Jules

Answer 3

如果forall是lambda的话，那么exists是什么？

当然是tuple（元组）啦！

在Martin-Löf类型理论中，你有Π类型，对应于函数/全称量化和Σ类型，对应于元组/存在量化。

它们的类型非常类似于您提出的内容（我在这里使用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

然而，这并没有涉及到参数性，据我所知，参数性和Martin-Löf类型理论是独立的。

对于参数性，人们通常会提到Philip Wadler的工作。

- Rotsor

---

谢谢! 又是一个出色的回答。正如你所说，无穷和与无穷积在我问的方式上确实不同，即它们导致了非参数性。这恰好说明了我对ML中的forall的关注点，因为它们是一种泛化，如果您可以根据类型进行调度，则可以创建非参数性。总和和乘积看起来像非常普遍和美丽的思想，我会再多读一些 :) - Jules