什么是类型量词？ [英] What are type quantifiers?

问题描述

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

  T Foo （T x）{return x; } 
  

在呼叫网站中，您可以执行以下操作：

  int y = Foo< int>（3）; 
  

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

  Foo :: forall T. T  - > T 
  

我听到有人说：在类型层面上，它就像是抽象的lambda。所以Foo是一个函数，它接受一个类型（例如int），并生成一个值（例如int类型的函数 - > int）。许多语言推断出类型参数，以便您可以编写 Foo（3）而不是 Foo （3）。

假设我们有一个类型的对象 f > T> T> ; Ť。我们可以用这个对象做什么，首先通过编写 f 将它传递给 Q 类型。然后我们返回一个类型为 Q - >的值。 Q 。但是，某些 f 是无效的。例如： f ：

  f  =（x => x + 1）
 f< T> =（x => x）
  

所以如果我们调用 f< ; int> 然后我们得到一个类型为 int - >的值。 int ，并且通常如果我们调用 f ，那么我们得到一个类型为 Q - > Q ，所以这很好。然而，一般的理解是， f 不是类型 f的所有T的有效事物。 T ，因为它根据你传递它的类型做了不同的。 forall的想法是，这是明确的 not 允许的。另外，如果forall是类型级别的lambda，那么存在的是什么？ （即存在量化）。由于这些原因，似乎所有和存在都不是类型层面的lambda。但那他们是什么？我知道这个问题很含糊，但是有人可以为我澄清这一点吗？

---

可能的解释如下：

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

 整数中的整数：P（n）
 
 整数中的整数：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]）... 
  
 
 
存在就像是一个无限的分解：
 
 pre>  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]）... 
存在（S，P）= P（S [0]）∪P（S [1]）∪P（S [ 2]）... 
  

所以所有的都是无限交集，存在是无限联合。它们的类型是：



  forall，exists :: Set< T> - > （T  - >类型） - >类型
  

例如多态身份函数的类型。这里 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 code> int - > INT 。这是有效的，因为 int - > int 也出现在无穷交集中。

我认为这很好地解决了这个问题，它清楚地解释了什么是和它是如何不同的lambda，但这种模式与我在ML，F＃，C＃等语言中看到的不兼容。例如，在F＃中，您可以使用 id< int> 来获取身份函数ints，这在这个模型中是没有意义的：id是一个函数的值，而不是一个函数的函数返回值函数。

blockquote>

---

具有类型理论知识的人可以解释究竟是存在还是存在？并且在多大程度上它是真正的lambda在类型级别？

解决方案

让我分别讨论您的问题。

• 调用所有类型级别的lambda是不准确的，原因有两个。首先，它是的lambda类型，而不是lambda本身。其次，lambda依赖于术语级别，即使它抽象了类型（类型级别上的lambda也存在，它们提供了通常称为泛型类型的类型）。
  存在类型基本上表示一种类型（所谓的见证）和一个术语，有时称为包。查看这些数据的一种常见方式是实现抽象数据类型。这里有一个简单的例子：
  
  

  pack（ int ，（λ x 。 em>，λ x 。 x ））：∃ Ť。 （ int → T ）× （ T → Int ）

  
  
  

  这是一个简单的ADT，其表示形式为 Int >并且只提供两个操作（作为嵌套元组），用于将ints转换成抽象类型 T 。例如，这是模块类型理论的基础。总之，通用量化提供了客户端数据抽象，而存在类型则提供了实现者 - 作为额外的说法，在所谓的 lambda立方体中，forall和箭头被推广到统一的数据集合。

的概念，并且同样存在，并且tupling可以被推广到σ -types（），其中T 1≠T 2 =Π（x：T 1）.T 2和T i。 （其中T1× T2 =Σ（x：T1）.T2 and∃ AT =Σ（A：））。在这里，类型&是类型的类型。

Many statically typed languages have parametric polymorphism. For example in C# one can define:

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

In a call site you can do:

int y = Foo<int>(3);

These types are also sometimes written like this:

Foo :: forall T. T -> T

I have heard people say "forall is like lambda-abstraction at the type level". So Foo is a function that takes a type (for example int), and produces a value (for example a function of type int -> int). Many languages infer the type parameter, so that you can write Foo(3) instead of Foo<int>(3).

Suppose we have an object f of type forall T. T -> T. What we can do with this object is first pass it a type Q by writing f<Q>. Then we get back a value with type Q -> Q. However, certain f's are invalid. For example this f:

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

So if we "call" f<int> then we get back a value with type int -> int, and in general if we "call" f<Q> then we get back a value with type Q -> Q, so that's good. However, it is generally understood that this f is not a valid thing of type forall T. T -> T, because it does something different depending on which type you pass it. The idea of forall is that this is explicitly not allowed. Also, if forall is lambda for the type level, then what is exists? (i.e. existential quantification). For these reasons it seems that forall and exists are not really "lambda at the type level". But then what are they? I realize this question is rather vague, but can somebody clear this up for me?

---

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.

---

Can somebody with knowledge of type theory explain what exactly are forall and exists? And to what extent is it true that "forall is lambda at the type level"?

解决方案

Let me address your questions separately.

• Calling forall "a lambda at the type level" is inaccurate for two reasons. First, it is the type of a lambda, not the lambda itself. Second, that lambda lives on the term level, even though it abstracts over types (lambdas on the type level exist as well, they provide what is often called generic types).

• Universal quantification does not necessarily imply "same behaviour" for all instantiations. That is a particular property called "parametricity" that may or may not be present. The plain polymorphic lambda calculus is parametric, because you simply cannot express any non-parametric behaviour. But if you add constructs like typecase (a.k.a. intensional type analysis) or checked casts as a weaker form of that, then you loose parametricity. Parametricity implies nice properties, e.g. it allows a language to be implemented without any runtime representation of types. And it induces very strong reasoning principles, see e.g. Wadler's paper "Theorems for free!". But it's a trade-off, sometimes you want dispatch on types.

• Existential types essentially denote pairs of a type (the so-called witness) and a term, sometimes called packages. One common way to view these is as implementation of abstract data types. Here is a simple example:

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

  This is a simple ADT whose representation is Int and that only provides two operations (as a nested tuple), for converting ints in and out of the abstract type T. This is the basis of type theories for modules, for example.

• In summary, universal quantification provides client-side data abstraction, while existential types dually provides implementor-side data abstraction.

• As an additional remark, in the so-called lambda cube, forall and arrow are generalised to the unified notion of Π-type (where T1→T2 = Π(x:T1).T2 and ∀A.T = Π(A:*).T) and likewise exists and tupling can be generalised to Σ-types (where T1×T2 = Σ(x:T1).T2 and ∃A.T = Σ(A:*).T). Here, the type * is the "type of types".

这篇关于什么是类型量词？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！