23

许多静态类型语言具有参数多态性。例如在 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).

假设我们有一个f类型为 的对象forall T. T -> T。我们可以对这个对象做的首先是Q通过写给它一个类型f<Q>。然后我们返回一个 type 的值Q -> Q。但是，某些f' 是无效的。例如这个f：

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

因此，如果我们“调用” f<int>，那么我们会返回一个带有 type 的值，int -> int一般来说，如果我们“调用” f<Q>，那么我们会返回一个带有 type 的值Q -> Q，所以这很好。但是，通常认为这f不是 type 的有效事物，因为根据您传递的类型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为有 type int -> int。这是有效的，因为int -> int也出现在无限交集。

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

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

4

3 回答 3

17

让我分别解决你的问题。

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

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

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

    包 ( Int , (λ x . x , λ x . x )) : ∃ 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）。这里，类型 * 是“类型的类型”。

于 2012-04-08T13:05:24.927 回答
8

一些评论来补充两个已经很好的答案。

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

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

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

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

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

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

  • Aforall a . foo不是“foo为每种类型生成一个实例”的东西，而是“在未知类型中泛型”a的单一类型。fooa

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

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

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

有关系统 F 的这种统一性/通用性方面的高级描述，请参阅 Fruchart 和 Longo 的 97 文章Carnap 对 Impredicative Definitions and the Genericity Theorem 的评论。有关在存在非参数构造的情况下系统 F 故障的更多技术研究，请参见Robert Harper 和 John Mitchell (1999)的 Girard's J 算子的参数化和变体。最后，从语言设计的角度来看，关于如何放弃全局参数化以引入非参数结构但仍然能够在本地讨论参数化的描述，请参见George Neis、Derek Dreyer 和 Andreas Rossberg 的Non-Parametric Parametricity， 2011 年。

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

最近有几个人在研究“无关性”的相关概念（lambda-abstractions，结果“不依赖于”参数），但仍然不完全清楚这与参数多态性的关系有多密切。一个例子是 Nathan Mishra-Linger 与 Tim Sheard 的工作（例如，纯类型系统中的擦除和多态性）。

于 2012-04-08T16:29:16.040 回答
7

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

为什么，当然是元组！

在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

但是，这根本不涉及参数性，AFAIK 参数性和 Martin-Löf 类型理论是独立的。

对于参数化，人们通常参考Philip Wadler 的工作。

于 2012-04-08T13:34:50.013 回答