类型级计算中的缩窄方法

理论计算机科学电子笔记174（2007）105-128www.elsevier.com/locate/entcs类型级计算中的缩窄方法。Tim Sheard蒂姆·谢尔德1，2波特兰州立大学计算机科学系。美国摘要Ωmega是一个实验系统，它结合了编程语言和逻辑推理系统的特点。Ωmega是一种具有无限计算层次的语言。一个级别的术语由下一个更高级别的术语分类（或类型化）。在本文中，我们报告使用两种不同的计算机制。在值级别，计算是通过归约来执行的，并且在很大程度上是不受约束的。 在所有更高的级别上，计算都是通过缩小来执行的关键词：程序设计语言，逻辑系统，定理证明，缩小，Curry-Howard同构。1引言最近有很多兴趣在或多或少传统的编程语言中利用类型系统中的Curry-Howard基于Curry-Howard同构的类型可以表达程序的精确属性。这些特性可以是功能性的或非功能性的。也就是说，它们可以限制程序的输出，或者产生输出所需的资源，或者两者兼而有之。Curry-Howard同构指出类型是命题（或性质），而程序是证明。这种同构指出了对同一现象的两种观点。当我们写prog1：：type1时，我们声明prog1的类型为type1，并且prog1是属性type1的证明。 通过推广类型的概念，我们可以使用类型来精确地描述程序的行为。1本文所报道的工作得到了美国国家科学基金会的资助CCF-0541447和CCF-06139692 电子邮件地址：sheard@cs.pdx.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.040106T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105为了有效地使用这个概念，我们必须把类型不仅仅看作是一种预测数据布局或表示的机制，或者是一种将值分类到相似组（所有整数，所有布尔值等）的机制。在Ωmega中，普通类型（如Int、String和函数箭头（->））扮演这些角色，但程序员也可以引入新类型，看起来像代数数据结构（列表，树等），但它存在于类型级别，而不是像普通代数数据那样存在于值级别。 这些类型扮演着传统类型所不扮演的新角色。它们不对值进行分类，而是用于描述属性，例如值级别数据的形状或函数应用程序消耗的资源。此外，Ωmega允许程序员编写操纵这些类型的程序，并且这些类型操纵程序不是在运行时执行，而是在类型检查时执行，以指导类型检查过程。声明一个程序的类型，说明该程序的一个属性，并检查程序是否具有声明的类型，证明它具有该属性。我们的目标是建立一个系统，在这个系统中，设计的规范、属性的定义、程序的实现以及程序是否符合它们的属性，都以一种连贯的方式捆绑在一个统一的系统中，在用户看来，这个系统就是一种编程语言。我们希望使用Ωmega作为广谱语言，能够处理抽象属性以及实现细节，其中属性和程序之间的联系是正式和精确的。语言Ωmega是我们构建这样一个系统的第一次尝试。这是一个正在进行的工作[23，24，29，33，32，30，31，34]。虽然它还没有达到我们下面列出的所有目标，但我们已经免费提供了它（www.example.com ）。http://www.cs.pdx.edu/2相关工作在值和类型级别上编写程序是一个奇怪但令人兴奋的想法！程序员在两个级别上编写程序，一个在运行时执行，另一个在编译时由类型检查器执行以强制执行属性。这种系统的设计空间很大。设计空间的探索角落包括逻辑系统，如归纳家族[12，15]，定理证明器（Coq [39]，Isabelle [25]），逻辑框架（Biferf [27]，LEGO[20]）和证明助手(ALF[22]，Agda [11]）。最近，设计空间探索已经发展到包括使用依赖类型来构建“实用”系统的工作，这些系统是部分语言，部分推理系统。 这些系统的设计差异很大。 有些人探索不同的部分大多数语言都有一些明确的设计目标，这些目标是语言设计者试图实现的。我们首先列出我们自己的Ωmega设计目标，然后尝试在设计空间中放置一些其他系统。在Ωmega，我们的设计目标包括：• 我们希望程序员和逻辑学家都能使用这个系统。我们希望我们的系统看起来和行为都像一种编程语言，但仍然是一种T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105107合理的逻辑• 当类型系统不允许一个程序时，我们希望程序员能够理解为什么程序被拒绝，并且能够理解如果可能的话如何修复程序（这很难！）• 值和类型之间应该有严格的区分。这允许实现使用类型擦除语义，因此类型（属性）在运行时不消耗任何成本。这是一个更普遍的政策的重要例子• 应该有一个为你所使用的方法付费。不需要太精确的程序，因此使用很少或不使用逻辑，应该产生很少或没有成本。那些属性必须受到高度限制的方法，编写和维护的成本将更高。• 语言必须能够表达各种计算。我们不应该抛弃语言特性，因为它们可能会使类型系统变得不可靠。相反，我们应该使用类型系统来区分健全的功能和不健全的功能。类型系统应该清楚地标记两者之间的边界。它应阐明控制不健全特征所需的义务，并支持和跟踪如何履行这些义务。结合编程语言和逻辑的当代方法的部分列表包括：• 卡宴Augustsson像许多依赖类型系统一样，它不区分值和类型。• 警句. McBride该系统是一个集成的编辑器类型检查器.使用Epigram的感觉更类似于使用证明编辑器，而不是编写程序。• RSP。Stump强调的是一种命令式的方法，而不是强调一种纯粹的功能性方法• DML。Xi和PfenningDML和Ωmega一样，将类型和值分开，但是索引类型的集合不能被程序员扩展，并且约束是通过一个固定的决策过程来解决的（而不是用户编写的类型级别函数）。• ATS。Chen和Xi发展了一种他们称之为应用类型系统的范式[42，10，9]。它与Ωmega的许多• 约束处理规则。Martin Sulzman应用了他定义约束类型系统的一般机制，约束处理规则，来构建一个具有类似目标的系统[38，36]。他的系统有一些很好的完备性结果，我们需要更多地了解。108T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105本文的技术重点是描述一种以前未探索过的在类型级别处理函数的机制：窄化。非技术性的重点是介绍几个重要的例子，说明类型如何描述属性。之所以选择这些例子，也是因为它们与狭义方法配合得很好。我们还将讨论几个问题，缩小的方法是无效的，并建议一些未来的工作。3程序设计语言与逻辑的结合Ω兆我们为Ωmega语言采用了以下结构。Ωmega是一种具有无限计算层次的语言：值，类型，种类，排序等。值级别的计算通过归约执行，并且在很大程度上是无约束的。所有更高级别的计算都是通过缩小来执行的，并且以多种方式受到约束。首先，所有类型级别及以上的“数据”都是归纳定义的数据（例如，没有数据库或原始数据）。其次，类型级别及以上的函数必须是归纳顺序的。这是对定义形式的限制，而不是对语言表达能力的限制。有关缩窄和这些约束的详细讨论，请参见第8每一层的术语按下一层的术语分类。因此，值是按类型分类的，类型是按种类分类的，种类是按排序分类的，等等。我们保持一个严格的阶段区分例如，没有类型可以依赖于值，也没有种类可以依赖于类型。程序员可以在每一层引入新的术语和函数，但任何特定的程序只能在有限的层上使用术语。利用Curry-Howard同构形式化了程序的性质。计算级别n的项被用作关于级别n+ 1的项的证明。我们使用索引类型来维护两个级别之间的严格和正式的连接，使用单例类型来维护值和类型之间的严格分离（更多信息将在第5节中介绍）。4一个简单的例子为了说明计算级别的层次结构，我们给出以下两个级别的例子。我们通过使用种类引入形式在类型级别上引入树状数据（自然数，Nat）。我们在类型级别上对这个数据（plus）编写一个函数。在类型级别和更高级别，我们通过用大括号（{和}）包围函数应用程序来区分函数应用程序和构造函数应用程序kind Nat：：*1其中Z：：NatS：：Nat ~> Natplus：：Nat ~> Nat ~> NatT. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105109{加上Z m} = m{plus（S n）m} =S {plus nm}然后，我们使用数据引入表单在值级别（Seq）引入数据。这些值的类型由自然数索引。这些索引描述了构造值的不变量-它们的长度出现在它们的类型中-考虑l1的类型。最 后，我们在值级别引入一个函数在Seq值（app）上。 应用程序的类型描述了其重要属性– there is a functional relationship between the lengths of its two inputs, and thelength of itsdata Seq：：*0~> Nat~> *0，其中Snil：：Seq aZScons：：a-> Seq a n-> Seq a（S n）l1= Scons 3（Scons5 Snil）：：SeqInt（S（S Z））app：：Seqa n ->Seqam->Seqa {plus nm}appSnil ys=ysapp（Scons x xs）ys = Scons x（app xs ys）自然数在类型级别上被证明是非常有用的。事实上，它是如此有用，以至于我们添加了特殊的语法糖来构建它们。我们有时写#0为Z，和#1为（S z），和#2为（S（S Z）），等等。也可以把（Sn）写成#（1+n），把（S（S n））写成#（2+n），等等。 当n为a变量5Ωmega简介在本节中，我们通过将Ωmega的特性与Haskell的特性进行比较和对比来介绍Ωmega的特性。我们假设对Haskell程序有基本的了解。功能：种类Kinds在类型级别或更高级别引入新的树状数据。一个kind声明引入了树形数据的构造函数和对这些结构进行分类的对象考虑两个新类型Set和终止日期：kindSet：： *1其中Univ：：Set拒绝：：设置时间：：Set~> Set~> Set加：：Set~> Set~> Setkind终止：：*1其中总计：：终止部分：：终止类型级的新树状数据由类型常量构造110T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105（Univ、Total和Partial）和类型构造函数（Times 和Plus）。类型Set和Termination对这些结构进行分类，如声明中显式显示的那样例如，Univ被Set分类，而Plus是一个从Set到Set到Set的构造函数。把操作符~>看作是类型级别的函数箭头。请注意，虽然Univ、Total或Partial存在于类型级别，但它们没有分类的值。相反，我们使用结构作为索引来值级数据，即。 类型如（TTotal）和（SUnivInt）。这些索引将指示值的静态（类型检查时间）属性。例如，类型为（TTotal）的值静态地保证具有Total属性，并且类型为（S UnivInt）的值静态地保证具有Univ属性。我们将很快介绍两个遵循这种模式的例子第一个例子是表示某种对象语言表达式的数据结构，其中类型为（ExpTotal）的Ωmega项表示在执行时总是终止的对象级项，类型为（ExpPartial）的项表示可能不会终止的对象级项。注意索引是一个语义不变式，出现在每个Exp的类型中。在定义Exp时明智地使用索引可以确保每个类型良好的项都保持不变。第二个例子通过类型（PatternUniv）或（PatternDeny）对表示模式的值进行分类。从语义上讲，模式是某个域上的谓词。即该域的某个子集。例如，在Haskell中，我们在case表达式中使用模式。模式（5，x）描述域例如（5，2）和（5，9）但不是（3，9）的整数对（因为模式常数5与值3不同）。我们将使用Set索引作为描述域中哪些集合与模式匹配的静态不变量考虑一个由简单对象、乘积和组成的域。Univ的索引意味着模式匹配每个值。索引为Deny意味着它们至少存在一个模式不匹配的值，可能很多。索引（乘以a b）表示模式匹配产品，产品的左部分匹配a，产品的右部分匹配b。类似的推理适用于具有（Plus ab）指标的不交和。功能：GADT。广义代数数据库允许构造函数拥有比Haskell中的数据声明所支持的类型更通用的类型。GADT很重要，因为它的额外的通用性允许程序员使用类型索引和见证（或证明）对象来表达类型的属性。GADT是支持Curry-Howard同构的机制单位为Ω。Ωmega中的数据声明定义了广义代数数据集（GADT），这是Haskell中可用的代数数据集的推广其特点是在数据声明中显式地用构造函数的完整类型对构造函数进行分类。由于GADT中构造函数的范围不限于仅应用于类型变量的类型构造函数，因此会出现额外的一般性。例如，考虑模式值级别类型：T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105111data Pattern：：Set~> *0 ~> *0where PVar：： String ->PatternUnivt PInt：： Int ->PatternDeny Int PPair：：Patterns1 a->模式s2 b->Pattern（Times s1 s2）（a，b）PWild：：Pattern UnivtPNil：： Pattern（PlusUniv Deny）[t]PCons：：Pattern s1 a->模式s2 [a]->模式（加拒绝（时间s1 s2））[a]注意，不同于像（Patterna b）这样的范围（其中只有像a和b这样的类型变量可以用作参数），范围包含复杂的实例化，如（PatternUnivt）。请注意，Pattern的第一个索引（Set）用于描述关于模式含义的不变量。变量模式（PVar“x”）：：（PatternUnivt）匹配所有类型t的所有值。但是，考虑嵌套模式：（PCons（PInt 4）（PVar“x”））：：模式（加拒绝（次拒绝Univ））[Int]它的类型告诉我们很多。它应该与[Int]类型的术语匹配。这样的对象可以被认为是不交和。该模式绝对不匹配左注入（为Nil对象保留它匹配某些右注入（即Cons对象），但不是全部。Cons对象可以被视为产品。权产品的一部分（列表的头部）只匹配一些东西（即值为4的整数，但不匹配其他整数，如3或7）。产品的正确部分（尾部）与一切相匹配。这一切都是嵌入式的术语！GADT模式是我们将在第10节中看到的更复杂的GADTPat的抽象。功能：类型功能。Kind声明允许我们在类型级别引入新的树型结构我们可以使用这些结构在值级别上对数据进行参数化，就像我们使用Pattern一样，或者我们可以在这些树状结构上进行计算。这样的函数是由模式匹配方程写的，在很大程度上，一个写函数的方式在值的水平上的数据在由Termination和Set分类的类型上有几个有用的函数：lub：：终止~>终止~>终止{lub总计x} = x{lub部分x} =部分allU：：Set~> Termination{allU Univ} =总计{allU拒绝} =部分{allU（Times x y）} = {lub {allU x} {allU y}}112T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105{allU（Plus x y）}={lub {allU x} {allU y}}union：：Set ~> Set ~> Set{union Univ a} = Univ{union（Times p1 p2）（Times q1 q2）} = Times {union p1 q1} {union p2 q2}{union（Times a b）Deny} = Times a b{union（Times a b）Univ} = Univ{union（Plus p1 p2）（Plus q1 q2）} = Plus {union p1 q1} {union p2 q2}{union（Plus p1 p2）Deny}= Plus p1 p2{union（Plus p1 p2）Univ} = Univ{union Deny x} = x与值级别的函数一样，类型函数lub、allU和union也是使用方程来表示的 在类型级别，我们使用方括号（{}）包围函数应用程序，以在类型级别（如（TreeInt）或（PatternUnivInt））将其与构造函数应用程序明确区分开来。函数lub是一个组合两个Termination的二元函数，allU将Set转换为Termination。 只有当Set的所有部分都是通用的时，它才返回Total。这两个函数都是严格的total（终止）函数。类型函数union联合两个Set。模式：证人。GADT可用于见证类型之间的关系属性。这是因为使用GADT机制引入的类型的参数可以扮演不同的角色。类型构造函数Seq的自然数参数（来自第4节）扮演着与普通ADT中的类型参数不同的角色。考虑二叉树数据类型的声明：data Tree a = Fork（Tree a）（Tree a）|节点a|尖端在此声明中，类型参数a用于指示Trees中有类型为a的子组件。 事实上，树是多态的。 任何类型的值都可以放在类型a的“子组件”中放置在那里的值的类型反映在树这与（Seq a n）中的n形成对比。相反，参数n用于表示抽象属性（代表名单）。当我们以这种方式使用类型参数时，我们称之为类型索引[41，44]而不是类型参数。我们可以使用GADT的索引来定义我们能想到的值级别数据作为类型级别属性的证明或见证。这是一个强有力的想法。考虑引入两个新的参数化类型Even和LE。请注意，这些是存在于值级别的普通数据结构，但在类型级别描述属性。data Even：：Nat ~> *0 whereEvenZ：：Even ZEven SS：：Even n -> Even（S（Sn））data LE：：Nat ~> Nat ~> *0其中LeZ：：LE Z nLeS：：LEn m-> LE（S n）（S m）这些声明引入了值级常量（EvenZ和LeZ）和构造函数（EvenSS和LeS）。让T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105113EvenZ：：Even #0（EvenSS EvenZ）：：Even #2（EvenSS（EvenSS EvenZ））：：Even #4LeZ：：LE #0 a（LeS LeZ）：：LE#1（S a）(LeS（LeS LeZ））：：LE#2（S（S a））我们把Z写成#0，把（S Z）写成#1，等等。为了强调我们应该把LE看作两个自然数之间的关系需要注意的重要一点是，我们可能会使用类型pes（LEnm）和（Evenn）作为profs的值，因为所有合法构造的值的类型只见证关于n的真实陈述，M. 例如，我们不能构建一个类型为（Even #1）的术语。这就是Curry-Howard同构的本 质我们可以将 （EvenSS EvenZ）： ：（ Even #2）看作是（ EvenSSEvenZ）具有类型（Even #2）的陈述，或者（EvenSS EvenZ）是属性（Even #2）的证明。所有这一切都直接来自于引入具有树状结构的新类型，以及在它们之上进行计算模式：单例类型。有时候，通过在值级别编写函数，在类型级别直接进行计算是很有用的。尽管类型不能依赖于值，但通过使用单例类型，这是可能的。其思想是在值世界中构建类型的完全独立的同构副本，但仍然保留两个同构结构之间的连接这种连接是通过用对应的类型世界类型索引值世界类型来维护的。这一点最好通过实例来理解。考虑把善良的纳特纳入价值世界通过使用数据声明定义类型构造函数SNatdata SNat：：Nat~> *0 whereZero：：SNatZSucc：：SNat n-> SNat（S n）three =（Succ（Succ（Succ Zero）：：SNat（S（S（S Z）这里，SNat的数据声明的值构造函数镜像了Nat的类型声明中的类型构造函数。我们通过使用SNat 该类型索引与值的形状一一对应。因此，SNat的类型索引精确地反映了它的形状。例如，考虑上面的例子三，并特别注意类型索引的结构，以及该类型的值的结构我们称这种相关类型为单例类型，因为任何单例类型都只有一个元素例如，只有Succ（Succ Zero）存在于类型SNat（S（S Z））中。可以为任何一阶类型（任何种类）定义一个单例类型所有的Singleton类型总是有I ~>*0的形式，其中I是我们要反射到值世界的索引。我们有时称单例类型为表示类型。我们不能过分强调单例属性的重要性每一个单例类型都完全刻画了它的单个居民的结构，单例类型中的值的结构完全表征了它的类型。因此，我们可以计算一个单例类型的值，并且在该值处的计算114T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105级别可以在类型级别表示属性通过使用单例类型，我们完全避免了使用依赖类型，其中类型依赖于值[35，28]。Pattern：A pun：Nat '. 我们现在定义类型Nat'，它在所有方面都同构于类型SNatNat'类型在Ωmega（和Haskell一样）值的命名空间和类型的命名空间是分开的。因此，有可能有相同的名称代表两个东西。一个在值空间，另一个在类型空间。我们通过定义双关语NatdataS：：Nat三值构造函数（Z：：Nat在Nat在这里，值的形状和类型索引是同构的。我们进一步利用这个双关语，通过在类型级别（#0，#1等）扩展用于编写自然数的语法糖。在值级别上将其转换为单例类型。因此我们可以写（#2：：Nat模式：计算程序和性能同步我们可以编写程序来计算一个索引值，并提供一个证明该值具有某些附加属性的证明。例如，当我们添加两个静态长度列表时，结果列表的长度与两个输入列表的长度相关，并且我们可以同时产生这种关系的见证data Sum：：Nat~>Nat~>Nat~>*0其中PlusZ：： Sum Z m mPlusS：：Sumn mz-> Sum（S n） m（S z）app1：：Seqa n ->Seqa m-> exists p. （Seq ap，Sumnmp）app1Snil ys=Ex（ys，PlusZ）app1（Scons x xs）ys ={Ex（zs，p）-> Ex（Scons x zs，PlusS p）}Ex是它将普通类型（Seqa p，Plusnm p）转换为存在类型（exists p）。(Seq a p，加上nm p））。功能：标签和标签。许多系统都有标签的概念。通常，标签是支持相等概念的唯一名称。很多时候，认为每个标签在一个相关类型的家族中具有唯一的类型是很方便的。作为T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105115作为第一个近似，考虑有限类型的Tag和它的单例类型Label：kind Tag = A |B |C |Ddata Label ： ： Tag ~> *0where A：：LabelAB：：标签BC ： ： 标签 CD ： ：标签D在这里，我们再次故意使用我们在Nat名称A、B和C在值和类型名称空间中定义。他们命名不同的，但在每个空间相关的对象。在值级别，每个Label都有一个类型索引来反映它的值。即A：：LabelA，B：：LabelB，C：：LabelC。所以在值命名空间中A是一个普通值，因为它是一个单例，它的类型（标签A）反映了它的结构。在类型（标签A）中，A是存在于类型级别的不同（但相关）对象，是由一种标签来分类的。这是一个非常有用的双关语。 值级别的每个标签都有不同的类型。因此，我们可以静态地区分两个不同的标签(or是相同的），通过观察它们的类型。上述方法的问题在于只有四个不同的标签。我们想要一个可数的无限标签集。我们不能显式地定义它，但我们可以在Ωmega内部构建这样一个类型作为原语。在类型级别，每个名称前面有反勾号（'）的合法标识符都是善良的标签。例如，在类型级别在价值层面，每个这样的符号我们写： 我们说值标签是单例类型，因此它们的值由它们的类型唯一确定 它们的值反映在它们的类型中。 这是一个强大的机制我们将在下一节中进行探讨。模式：对象语言中的绑定。变量绑定是富语言建模时的一个长期问题。我们的绑定方法是使用双管齐下的方法，同时使用标签和de Bruijn指数。这种方法与记录结构的概念有关。为了定义记录，我们分两步进行。我们在类型级别定义了一种新的类型，称为行，然后我们在值级别定义了一种新的数据结构（记录），它是按行分类的。kind Row：：*1~> *1其中RNil：：RowaRCons：：a ~> Row a ~> Rowa kind HasType = Has Tag *0在类型级别上，XML 只不过是类似于多态列表的结构行的示例包括：（RConsInt（RCons BoolRNil））类型行和（RCons #5RNil）Nat行，以及（RCons（Has这种类型是由行kinded。 类Row是一个高阶类，它的分类是（*1~>*1）。因此，Row必须应用于一种类型（例如*0，Nat，116T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105或HasType）格式良好（参数指示存储在行中的类型的种类）。HasType只不过是一对类型。第一个组件必须是Tag，第二个组件必须是普通类型（如Int或String）。 为了在价值层面上定义记录数据，我们进行如下操作。data Record：：RowHastype ~> *0 whereRecNil：： Record RNilRecCons：：Label a -> b -> Recordl-> Record（RCons（Has a b）l）record1：： Record（RCons（Has通过将构造函数RecCons和RecNil应用于适当的值来构造记录数据。参见上面的示例记录1。请注意在值级别使用标签（标记的de Bruijn索引通过使用完全相同的结构来实现。我们构建了一个值级别的数据结构Exp，索引为（Row HasType）。这个索引唯一地标识出现在术语中的变量，在术语类型中。如果语言具有绑定结构（即任何类型的作用域机制，如lambda），或let），则变量的绑定位置由其在环境中的位置确定（这就是使其类似de Bruijn的原因）。例如，让值级别数据Exp有两个索引： Exp：：Row HasType ~> *0 ~> *0。解释一个术语以类型（Expr t）作为类型为t的项，其自由变量由以下描述：R. 例如，考虑具有以下类型的项：Exp（RCons（Has这个术语有两个自由变量，分别命名为这个术语应该出现在一个更大的上下文中，其中变量这种混合方法实现了两件事。标签有读者，但位置或德布鲁因指数是什么计数。这使得在正式操作术语时不必进行alpha重命名，但标签在检查术语及其类型时为读者提供了一些视觉线索。标记、标签、行和Hastype构建的对象看起来非常像类型环境。Row和HasType非常有用，我们已经为打印它们构建了特殊的语法糖。例如，Rec（RCons（Has'x Int）（RCons（Has 'a Bool）RNil））打印为Rec 'x：Int，' a：Bool}。Row和HasType的语法糖用方括号替换RCons和RNil，用冒号替换Has 一种类型，按行分类，其（最终）尾部不是RNil（即， 类型变量）打印时带有尾随的分号。比如说，Rec（RCons（Has'xInt）（RCons（Has 'a Bool）w））打印为Rec 'x：Int，'a：Bool; w}。使用这种表示法，我们前面的例子看起来像：Exp'f：b->t，'x：b; d}t现在我们理解了这个机制，让我们用它来定义对象语言T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105117使用绑定结构跟踪其元级别类型中的自由变量对象语言（Lam envt）表示简单类型的lambda演算。dataLam：：Row HasType ~> *0 ~>*0其中Var：：Label s -> Lam（RCons（Hasst）env）tShift：： Lamenvt-> Lam（RCons（Hass q）env）tAbs：： Label a -> Lam（RCons（Has as） env）t-> Lam env（s->t） Apply：： Lam env（s->t）-> Lam envs-> Lam envtLam，env的第一个索引是一个Row，用于跟踪其变量，第二个索引t用于跟踪术语的对象级别类型例如，具有变量x和y的项可能具有类型Lam'x：Int，'y：Bool; u} Int。这种方法的关键是在函数（Abs）和变量（Var）的类型化中使用Row和Hastype。考虑Var构造函数。 为了构造一个变量，我们简单地将Var应用于一个标签，它的类型反映了这一点。例如，下面是一个短与Ωmega解释器的交互式会话。prompt> Varforall a（u：Row HasType）. Lamprompt> Varforall a（u：Row HasType）. Lam变量的行为类似于Bruijn指数。用Var创建的变量就像自然数0。一个变量可以通过后继操作符Shift提升到下一个自然数。 要理解为什么这是有用的，请考虑这两个示例在同一索引位置具有不同的名称。如果这两个变量都用在同一个lambda项中，它们就会发生冲突。要将变量的位置移动到不同的索引，我们使用Shift：：Lam u a-> Lam {v：b; u} a构造器。而不是用自然数计数（如de Bruijn索引）我们用行来“计数”，记录它的符号名称和类型。下面是我们如何定义在同一环境中使用的两个变量x和yx ：：y ：：Lam{u：a类型系统现在跟踪表达式中的变量。z *z =（Apply（Var（y））我们已经发现了许多利用Ωmega特性的其他有用模式。Ωmega还有几个特性我们还没有讨论，特别是使用见证类型作为静态约束，以及管理118T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105他们但在本文的其余部分，我们将重点放在缩小Ω兆的使用。6类型检查Ωmega使用类型检查和类型推断的组合。类型推断，如Ωmega中实现的，只能将Hindley-Milner类型分配给术语，并且只能在代数数据集上工作（与广义代数数据集相反），因此类型检查是许多Ωmega程序中的正常类型模式在类型检查期间，信息可以在两个方向上流动。我们可以计算一个术语的类型，然后检查它是否与它声明的类型一致，或者我们可以使用声明的类型来建议一个术语的类型，然后遍历术语计算与该建议一致的类型。在某些系统中，每个术语都有一个主类型，该术语的所有其他类型都是该主类型的“实例”。但这样的制度可能限制性太大。检查发现一个术语是否具有特定的类型，即使它可能还有其他类型。类型声明声明了应该选择多个类型中的哪一个作为该术语的类型。每个词都有一个类型（也就是一个意义），即使它可以有不止一个类型。在类型检查时，我们经常会问两个类型（b和c）是否相互一致（bc）。考虑函数应用的Γf：c→d rx：b b/crfx：d类型检查器执行计算来回答一致性问题。不同的语言提出不同的问题。一些问题有简单的是/否答案，其他搜索找到满足某些标准的特定值，或将复杂的项简化为简单的范式。例如，在像Pascal这样的单态语言中，相互一致意味着结构上相等。在像Haskell这样的多态语言中，相互一致意味着b和c是可统一的。在具有子类型的语言（如Java）中，相互一致意味着b是C.在Ωmega中，consistent意味着语义等价。由于使用了类型级函数，句法等价不再是足够的。类型不再是静态的自由代数，而是动态的计算。这种现象的一个非常简单的例子是第4节中的app函数。考虑对第二个子句进行类型检查。app：：Seq a n-> Seq am-> Seq a {plus n m}app（Scons x xs）ys=Scons x（app xs ys）从声明中，我们知道模式（Sconsxxs）具有类型（Seq a（S b）），其中（n =（S b）），因此我们必须证明右侧具有类型：Seqa{plus（S b）m} 。 计 算 右 边 的 类 型 ， 我 们 得 到 ： Scons x （ app 2 xs ys ） ： ： Seqa（S{plusb m}）。类型（Seq a{plus（Sb）m}）和（Seqa（S{plusbm}））通常是对b和m的查找，使得{plus（S b）m}在语义上等于（S {plus b m}）。T. Sheard/Electronic Notes in Theoretical Computer Science 174（2007）105119如果我们允许在类型级别上进行计算，我们将需要一种计算机制，它可以执行一个简单 的 ncestonsuchas （ Seqa{plus（Sb） m}）n（ Seq a（S {plus bm}））。我们知道有几种选择。首先，可以使用还原和统一的组合。第二，可以使用蕴涵。第三，可以使用约束求解，第四，可以使用缩小。• 减少统一。为了检查一致性，我们将这两项简化为范式，然后统一范式。这就是Morrisett所采取的方法[13]。不幸的是，简单的一致性检查，如（{plus bm}m）不能回答，因为双方都处于正常形式，统一不求出正确的解b=Z。• 蕴含。通过在逻辑上表达类型级别的计算，我们可以使用蕴涵机制（例如解析或高阶模式匹配）来解决一致性检查。在逻辑框架中就是这种情况[26]。这种选择与我们对用于在值和类型级别定义函数• 约束求解。通用的约束求解系统可以用来确定等价性。将约束求解器应用于类型检查的一个例子是Sulzman• 缩小范围。缩小结合了减少和统一的力量。窄化是函数逻辑语言Curry的主要计算机制[17，16]。与统一不同的是，被比较的项可以包含函数，与简化不同的是，被 简 化的 项 可 以 包含 变 量 。 窄化 查 找 在 其术 语 中 的 一 些自 由 变 量 的绑 定Narrowing是一个特殊用途的约束求解系统，当在类型级别上有函数我们的设计目标之一是一致性。集成系统的美妙之处在于用户只需学习一种工具。如果它有许多不同的模式，每种模式都需要不同的技能，那么整合的好处就失去了。因此，即使我们使用不同的机制在编译时和运行时执行程序，我们也希望两者的用户界面是相同的在类型检查时，窄化是执行的最佳选择运行时和编译时计算的接口是递归方程的编写7缩小的工作原理缩小结合了减少和统一的力量窄化查找在被窄化的项中的一些自由变量的绑定，一