什么是类型量词？

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和存在并不是真正的"类型级别的lambda".但那他们是什么？我意识到这个问题相当模糊,但有人可以为我清楚这一点吗？

---

可能的解释如下:

如果我们看一下逻辑,量词和lambda是两回事.量化表达式的一个示例是:

forall n in Integers: P(n)

因此,forall有两个部分:一组量化(例如整数)和一个谓词(例如P).Forall可以被视为更高阶函数:

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

带型号:

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

存在具有相同的类型.Forall就像一个无限的连接,其中S [n]是集合S的第n个元素:

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

存在就像一个无限的分离:

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

如果我们对类型进行类比,我们可以说∧的类型模拟是计算交集类型∩,以及∨计算联合类型type的类型.然后我们可以定义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是一个无限的交集,存在是一个无限的联合.他们的类型是:

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>了获取int上的identity函数,这在这个模型中没有意义:id是值的函数,而不是返回值的函数的函数.

---

有类型理论知识的人能解释究竟是什么样的并且存在吗？在什么程度上"forall是lambda在类型级别"？

Answer 1

让我分开回答你的问题.

• 由于两个原因,将forall称为"类型级别的lambda"是不准确的.首先,它是lambda 的类型,而不是lambda本身.其次,lambda存在于术语级别,即使它在类型上抽象(类型级别上的lambdas也存在,它们提供通常称为泛型类型的东西).

• 通用量化并不一定意味着所有实例化都具有"相同的行为".这是一种称为"参数"的特殊属性,可能存在也可能不存在.普通的多态lambda演算是参数化的,因为你根本无法表达任何非参数行为.但是如果你添加像typecase(也就是内涵类型分析)这样的结构,或者选择一个较弱的形式,那么你就会失去参数.参数化意味着很好的属性,例如,它允许在没有任何类型的运行时表示的情况下实现语言.它引出了非常强大的推理原则,例如参见Wadler的论文"免费定理".但这是一种权衡,有时你想要对类型进行调度.

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

  包(诠释,(λ X.X,λ X.X)):∃ Ť.(Int → T)×(T → Int)

  这是一个简单的ADT,其表示形式为Int,并且仅提供两个操作(作为嵌套元组),用于转换内插和抽出类型T的内容.例如,这是模块类型理论的基础.

• 总之,通用量化提供了客户端数据抽象,而存在类型提供了实现者端数据抽象.

• 作为补充说明,在所谓的lambda立方体中,forall和箭头被推广到Π型的统一概念(其中T1→T2 =Π(x:T1).T2和∀AT=Π(A:*) .T)并且同样存在并且可以将元组推广到Σ-类型(其中T1×T2 =Σ(x:T1).T2和∃AT=Σ(A:*).T).这里,类型*是"类型的类型".

Answer 2

一些评论补充了两个已经很好的答案.

首先,我不能说forall在类型级别是lambda,因为在类型级别已经存在lambda的概念,并且它不同于forall.它出现在系统F_omega中,系统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).如果在类型级别有计算,那么如果要确保终止类型检查,则需要控制它(否则你可以定义类型(lambda t. t t) (lambda t. t t).这是通过使用"类型级别的类型系统"或者种系统.prod将种* -> * -> *,只有类型中在一种*可通过值有人居住,类型在较高的实物只能在类型级别上.lambda (c : k) . ....是一种类型的级抽象,不能是值的类型,并且可以以任何形式生活k -> ...,同时forall (c : k) . ....对某些类型的多态性进行分类,c : k并且必须是地面类型*.

其次,forall系统F和Martin-Löf型理论的Pi类型之间存在重要差异.在系统F中,多态值在所有类型上都做同样的事情.作为第一个近似值,您可以说类型的值forall a . a -> a将(隐式)将类型t作为输入并返回类型的值t -> t.但这表明在这个过程中可能会发生一些计算,但事实并非如此.从道义上,当实例类型的值forall a. a -> a到类型的值t -> t,该值也不会改变.有三种(相关的)方式来考虑它:

• 系统F量化有类型擦除,你可以忘记类型,你仍然会知道程序的动态语义是什么.当我们使用ML类型推断离开多态性抽象和实例化隐含在我们的节目,我们并不真正让推理机"填补了我国在程序漏洞",如果你认为"方案"作为将要运行的动态对象并计算.

• A forall a . foo不是" foo为每种类型生成实例的东西a,而是foo"在未知类型中为"通用" 的单一类型a.

• 您可以将通用量化解释为无限连接,但是存在一个统一条件,即所有连词具有相同的结构,特别是它们的证明都是相似的.

相比之下,Martin-Löf类型理论中的Pi类型更像是功能类型,它们会带来某些东西并返回某些东西.这就是为什么它们不仅可以轻松地用于依赖类型,而且还依赖于术语(依赖类型)的原因之一.

一旦你关注那些正式理论的健全性,这就具有非常重要的意义.系统F是不可预测的(包括所有类型的forall量化类型量化,包括其自身),并且它仍然合理的原因是这种通用量化的一致性.虽然从程序员的角度来看引入非参数构造是合理的(并且我们仍然可以推断通常非参数语言中的参数化),但它很快就会破坏底层静态推理系统的逻辑一致性.Martin-Löf 预测理论更容易证明是正确的并且以正确的方式延伸.

有关系统F的这种一致性/通用性方面的高级描述,请参阅Fruchart和Longo的97篇文章Carnap关于Impredicative Definitions和Genericity Theorem的评论.有关存在非参数构造的系统F失效的更多技术研究,请参阅Robert Harper和John Mitchell(1999)的Girard J算子的Parametricity和变体.最后,从语言设计的角度来看,关于如何放弃全局参数以引入非参数构造但仍能够在本地讨论参数化的描述,参见George Neis,Derek Dreyer和Andreas Rossberg的非参数参数, 2011.

关于"计算抽象"和"统一抽象"之间差异的讨论已经通过表示变量绑定器的大量工作而得以恢复.绑定构造感觉就像一个抽象(并且可以通过HOAS样式中的lambda抽象来建模)但是具有统一的结构,使得它更像是数据骨架而不是一系列结果.这已经有很多讨论,例如在LF社区,Twelf中的"代表性箭头",Licata&Harper的工作中的"正箭头"等.

最近有几个人正在研究相关的"不相关"概念(lambda抽象,其结果"不依赖于"论证),但仍然不完全清楚这与参数多态性有多密切相关.一个例子是Nathan Mishra-Linger和Tim Sheard的工作(例如纯粹系统中的擦除和多态).

Answer 3

如果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的工作.