haskell - 什么是类型量词？

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) .

假设我们有一个对象 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 是类型级别的 lambda，那么存在什么？ (即存在量化)。由于这些原因，似乎 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 和存在的吗？ “forall 在类型级别上是 lambda”在多大程度上是真的？

Answer 1

让我分别解决你的问题。

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

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

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

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

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

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

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