《Haskell中的类型安全和编译器可靠性》

理论计算机科学电子笔记174（2007）23-39www.elsevier.com/locate/entcsHaskell中的类型安全代码转换Stefan Monnier2Universit'ed'eMontr'ealDepartem entd摘要使用类型化中间语言可以显著提高编译器的可靠性。通过对每个转换阶段产生的代码进行类型检查，可以识别编译器中的错误，否则这些错误很难找到。我们建议在编译中更进一步地使用类型，通过验证转换本身是类型正确的，也就是说，它不可能产生输入一个类型良好的术语。我们的方法基于高阶抽象语法（HOAS），表示程序中的对象语言中的变量表示的元变量。我们使用一种表示，该表示使用广义代数数据类型（GADT）来说明对象语言的类型系统。这样，对象语言的完整绑定和类型结构就暴露给宿主语言的类型系统。在这个设置中，我们使用GADT中编码的类型正确性证明的见证人，在Haskell的类型系统中编码CPS转换的类型保留属性关键词：编译，程序验证，类型系统，高阶抽象语法1介绍虽然还有很长的路要走，直到他们成为数字系统中的常见的地方，正式的类型系统可以说是用于开发软件的最成功和最流行的形式化方法，自Java兴起以来更是如此。出于这个原因，尝试逐步增强类型系统以使它们能够证明更复杂的属性是很有兴趣的。因此，随着类型系统技术的进步，出现了新的需求和新的机会。这些需求之一是确保从源代码到机器代码的翻译的忠实性。毕竟，如果我们的编译器可以把源代码转换成一些无关的机器代码，为什么还要费心证明源代码其中一个机会就是使用类型来满足这种需求。这就是我们正在努力做的。1电子邮件地址：guillelj@iro.umontreal.ca2电子邮件地址：monnier@iro.umontreal.ca1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.03624L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23类型化中间语言已经被用于编译器中的各种目的，例如类型导向优化[8，23，15]，健全检查以帮助捕获编译器错误，以及最近帮助构造生成的代码验证某些属性的证明[11，6]。通常，源级别类型以数据结构的形式表示在那些类型化表示中，这些数据结构必须被仔细地操纵以在代码通过编译的各个阶段前进时使它们与它们注释的代码保持同步。这有几个缺点：• 很明显，额外的工作会减慢我们的编译器。为了最大限度地减少影响，类型语言和类型注释必须非常仔细地设计和编码，使用散列consing，显式替换和其他优化技术[18]。• 有时候，需要更新类型注释可能会使优化不切实际，例如，因为必要的类型信息不是立即可用的，因此需要重构算法。• 需要在不同的设计权衡中做出选择：要么只放置尽可能少的类型注释以减少上面第一个问题的影响，要么相反，在所有地方添加类型注释以减少遇到上面第二个问题• 只有当我们运行类型检查器时才能检测到错误，但是尽可能频繁地运行它会使编译器的速度更慢。• 这相当于测试我们的编译器，因此bug可能潜伏，未被发现。为了避免这些问题，我们希望将类型化中间语言的源类型表示为类型而不是数据。这样，我们编写编译器的语言的类型检查器就可以一劳永逸地验证我们的编译器是否正确地保留了类型。编译器本身可以全速运行，而不必操作和检查任何更多的类型。这也给了我们更早的检测错误引入了一个不正确的程序转换，并在一个非常细的颗粒，因为它相当于运行类型检查器后，每一个指令，而不是只在阶段之间。类型保留参数已经被引入到编译器的实现中，使用类型化程序表示[2]。但据我们所知，这里介绍的工作是第一次尝试使用Haskell这样广泛使用和支持的语言正式建立类型保持属性，工业强度编译器可用。这项工作遵循与[9]类似的目标，但我们只试图证明我们的编译器的静态语义的正确性，而不是完整的动态语义。作为回报，我们希望使用一种更实用的编程语言，并希望将注释限制在最低限度，这样大部分代码应该处理编译而不是证明。此外，我们已经开始这项工作从前端，并使我们的方式向后端，而勒罗伊的工作已经开始与后端。我们的贡献如下：• 我们展示了一个用Haskell编写的保持类型的CPS翻译，L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2325GHC编译器验证了类型保持的属性。• 我们将抽象语法树的广义代数数据类型（GADT）表示的经典玩具示例扩展到具有绑定的完整语言• 我们在中间表示中使用高阶抽象语法（HOAS），遵循[24]，我们展示了如何将这种技术与GADT结合起来，以及如何使用Template Haskell构建这样的术语。本文的其余部分组织如下。我们回顾广义alge-algebra datashees和高阶抽象语法的概念。二、第3节介绍了CPS转换，陈述了它满足的类型保持属性，然后展示了我们如何在Haskell中对其进行编码。第4节介绍了一些替代方法，以及我们遇到的一些问题的解决方案第5节提到相关工作和SEC。6结束2背景在本节中，我们使用GADT和高阶抽象语法为一个简单的源语言开发一个有类型的程序表示，该源语言是一个带有对和整数的简单类型λ-演算（这里称为λ→）。我们简要地描述了用于操纵这样一个表示的编程技术的基础上沃什-伯恩和Weirich2.1广义代数数据集广义代数数据集（GADT）[25，3]是代数数据集的一种推广，其中给定数据类型的各种数据构造函数的返回类型不需要相同-它们可以在定义的类型构造函数的类型参数中不同。类型参数可用于对有关所表示的值的附加信息进行编码。为了达到我们的目的，我们使用GADT来表示抽象语法树，并使用这些类型注释来跟踪表达式的源代码级别的类型。考虑图1中定义的语言λ→。 λ→的片段与整数可以在GADT中表示如下：data Expt其中：：Int-> ExpIntPrim：： PrimOp -> ExpInt-> ExpInt-> ExpInt If 0：： ExpInt-> Expt-> Expt数据PrimOp =添加|子|Mult这种Exp数据类型不仅定义了抽象语法，还编码了我们语言的类型规则。例如，一个语句如Γe：τ在Haskell中被表示为e：：Exp τ。 环境Γ保持隐式。 还要注意，Exp t类型的表达式表示源类型t的λ→表达式，其中我们（任意）选择Haskell类型t来代表相应的λ→类型t（例如， 我们使用Haskell类型Int来表示λ→类型int。将这种编码扩展到变量和λ情况并不简单26L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23（类型） τ：：= τ1→τ2|int|τ1×τ2（type env）Γ：：=·|r，x：τ（primops）p：：= + | − |×（exp）e：：= x| λx：τ1.e：τ2|e1e2|（e1，e2）|πie|我|e1p e2| 如果0e1e2e3类型规则r（x）=τrx：ττ，x：τ1τe：τ2τ1→τ2Γe1：τ1→τ2τ1e2：τ2Γε1：τ1Γε2：τ2Γ（e1，e2）：τ1×τ2Γe1：intΓe2：intΓe1pe2：intτ1×τ2Γπie：τiΓi：int1：int 如果0 e1e 2 e3：τ，则τ 2：τFig. 1. λ →语法和静态语义因为我们保持了Γ的隐式。当然，我们可以尝试像ExptΓ中那样使Γ显式化，但这很快就会变得很麻烦，因为它可能需要在类型级别上具体化变量，并编码诸如弱化和交换之类的结构规则。因此，我们使用高阶抽象语法，它允许我们保持Γ隐式。2.2高阶抽象语法高阶抽象语法（Higher-Order Abstract Syntax，HOAS）[14]是一种程序表示，其中对象语言中的变量使用元变量表示。例如，我们源语言中的函数将使用Haskell函数表示;因此我们可以扩展程序表示以考虑λ→函数，如下所示：data Expt其中...Lam：：（Exps -> Expt）-> Exp（s ->t） App：： Exp（s ->t）-> Exps-> Expt从这个定义中可以明显看出，λ→中函数的类型规则可以直接用Haskell的函数类型规则来表达在高阶项上定义递归函数通常是困难的问题来自于这样一个事实，为了检查术语为了减轻这种困难，使用一种消除形式是有用的，通常称为变形（或迭代器;我们在这里互换使用这两个术语，尽管它们在其他地方有更具体的含义[24]）。分解封装了递归结构的遍历;更确切地说，它是一个（高阶）函数，给定一个初等运算，L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2327data ExpF a其中Lam：：（a t1 -> a t2）-> ExpF（a（t1 -> t2））App：：a（t1 -> t2）-> a t1-> ExpF（a t2）对：：a t1 -> a t2->Expf（a（t1， t2））Fst：： a（t1， t2）->ExpF（a t1）Snd：： a（t1，t2）-> ExpF（a t2）Num：：Int->ExpF （ aInt ） Prim ： ： PrimOp -> aInt-> aInt-> ExpF （ aInt）If 0：：aInt-> at-> at-> ExpF（at）data Rec a b t= Roll（a（Rec a b t））|放置（b t）类型Exp a t= Rec ExpF a t图二. λ →的有类型的参数表示对单个元素执行，将此操作应用于结构的每个元素(The最熟悉的变形的例子是列表上的折叠函数在这项工作中，我们利用Fegara和Sheard在本节的剩余部分，我们简要地展示了如何使用这样的迭代器，以及必须对上面显示的（朴素的）程序表示进行哪些修改，并通过一个简单的例子来说明它的使用。图2显示了我们使用的表示它在两个方面不同于朴素(i) 它被分为ExpF和Exp两种类型，以使表示的递归结构显式。ExpF类型是由Exp类型定义的递归形式是通过应用一种定点运算符获得的，该运算符由类型构造函数Rec表示。(You可以忽略数据构造函数Place，它由迭代器内部使用;如果你好奇的话，请参阅[5(ii) 这种表示在类型变元a中是参数化的，也就是说，源类型t的λ→项由类型λa的项表示。Expa t，其中t是表示t的Haskell类型。 当应用变形时，类型变量a使用表示与术语关联的信息的类型实例化（例如，在下面的pretty-printer示例中，该信息是表示为字符串的术语的文本表示）。图3显示了迭代器的类型及其应用示例内部函数xmapExpF、cata和iter取自[24]，并适用于类型化表示的情况。pretty-printer实现由两个函数组成：showAux，它显示语法树的单个节点，showE，它显示整个树，并通过迭代器的应用获得事实上，在我们的高阶程序表示中，程序变量被表示为Hasell变量，因此没有与它们相关的标识符。在遍历过程中，pretty-printer为变量分配标识符。与术语相关联的信息是其文本表示，即参数-28L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23xmapExpF：：（xmapExp F）（at->bt，bt->at））->（不适用。（ExpF（at）->ExpF（bt），ExpF（bt）->ExpF（at）cata* *（不好意思。（ExpF（at）->at））->（at. Expat->at）地点r* *（不好意思。 实验F（bt）->bt）->（bt. （（a. Expat）->bt））showAux：： ExpF（[String] -> String）->（[String] ->String） showAux（Stringn）（v：vars） = shownshowAux（App x y）vars =“（“++（x变量）++““++（y变量）++“）”showAux（Lamz）（v：变量）=（fn“++v++“=“++（z（const v）vars）++“）...showE：：（a. Exp at）->StringshowE e =iter showAux evars其中vars ='a '.. 'z']++.图3.第三章。使用Fegara和Sheard迭代器的Pretty-printer实现一个人的性格，一个人的性格。Expat实例化为Exp（[String] -> String）t. 在一个命令式语言中，我们会简单地使用一个gensym工具，但是Haskell是无侧写的，我们必须在display函数中线程化一个可用标识符列表。3CPS转换在本节中，我们将介绍本文的核心贡献：CPS转换的实现，其中使用Haskell的类型系统来编码该实现正确保留类型的证明。我们按以下步骤进行。我们首先展示CPS转换的理论形式;然后定义目标语言λK的类型化表示;然后展示如何使用存在类型和GADT来编码类型对应的见证;最后展示如何使用GADT来编码类型与其CPS形式之间的函数依赖3.1理论转换为连续传递风格（CPS）命名所有中间计算结果，并使程序的控制结构显式。在CPS中，函数不向调用者返回值，而是通过应用continuation来传达其结果，continuation是表示“程序的其余部分”的函数，即将消耗产生的值的计算的上下文。CPS转换的目标语言（这里称为λK）具有以下内容L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2329Ktype<$int）=intK型<$τ1×τ 2）=K型<$τ1）× K型<$τ2）K型<$τ1→τ2）=（K型<$τ1）×（K型<$τ2）→0））→0K <$x）κ=κ xK <$λx：τ1，e：τ2）κ = κ（λ（x，c）：K型<$τ1）×（K型<$τ2）→0）。K<$e）c）K <$e1e2）κ = K <$e1）（λx1. K∈2）（λx2. x1（x2，κ）K <$（e1，e2））κ = K <$e1）（λx1. K∈2）（λx2. k（x1，x2）K <$πie）κ = K <$e）（λx. 设x=πixinκ x）K <$i）κ=κ iK <$e1pe2）κ = K <$e1）（λx1. K∈2）（λx2. 设x3=x1p x2inκx3））K <$if0e1e2e3）κ = K <$e1）（λx. 如果0x（K <$e2）κ）（K<$e3）κ））Kprog<$e）= K <$e）（λx. 停止（x）见图4。 CPS转换语法：（类型） τ：：= τ→0|int|τ1×τ2（type env）Γ：：=·|r，x：τ（值）v：：= x|我|λx：τ。e|（v1，v2）（primops）p：：=+| − |×（exps） e：：= letx = vine|设x = πivine|设x = v1p v2in e| v1v2|如果0 v e1e2|停止v它与λ→的不同之处在于它的句法结构被分为两个句法范畴：前值和值。值代表那些可以绑定到变量的东西表达式由一系列声明（由let形式引入）组成，后面是函数应用程序，条件表达式或特殊形式的halt，它表示程序产生的最终函数不返回调用者的事实在其类型中被反映为τ→0。图4显示了CPS转换本身。它被定义为三个功能。主函数K <$−）κ将λ→表达式转换为CPS形式表达式，给出一个延拓κ。对于λ→中的每一个类型，函数K类型<$−）给出λK中相应的类型。(Note该函数用于转换K <$λx：τ1.e：τ2）情况下的类型注释）。最后，Kprog<$−）通过安排将最终结果传递到特殊形30L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23式halt来转换整个程序。L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2331Γ（x）=τΓ<$Kx：τr， x：τKeΓ<$Kλx：τ。e：τ→0ΓKi：inti。 ΓKvi：τiΓK（v1，v2）：τ1×τ2ΓKv1：τ→0ΓKv2：τ俄克拉荷马v1v2rKv：τr， x：τKeΓKletx=vineΓ<$Kv：τ1×τ2Γ， x：τi<$KeΓ<$Kletx=πivineΓKv1：intΓKv2：intr， x：intxeΓKletx=v1pv2ineΓKv：intΓKe1ΓKe2如果0ve1e2，ΓKv：τKhaltv图五. λK的值和表达式的类型规则3.2类型保持图中所示的结构示意图。5个定义的两个字判断gments：rK v：τ这是一个简单的方法;当我们使用它时，我们会发现它是一个简单的方法。在其最简单的形式中，类型保留声明，如果程序在λ→，那么CPS转换后的程序也将是良好类型的：Orem3.1（CPS型）If·e：τ，then·Kproge）。为了证明上述定理，证明一个更强的性质是有用的，该性质建立了λ→中的类型与λK中的类型之间的对应。我们可以正式地把这种对应关系表述如下：在3.2（λ→- λ K t y p e c o r e s p o n d e c e）条件下 λc. K<$e）c：（K型<$τ）→0）→ 0。请注意，CPS中的表达式被3.3程序表示图6显示了λK的类型化表示。理想情况下，我们希望定义两个相互递归的类型，ValK和ExpK，分别表示值和表达式的语法类别。然而，我们的定点运算符（Rec，见图2）只能应用于一个类型，所以我们对两个语法类别使用相同的类型。（或者，人们可能更愿意将递归方案扩展到两个或更多类型的情况，但我们在这里不尝试这样做表达式和值之间的区别实际上并没有丢失：我们利用GADT来恢复这种区别，通过将相应的语法约束编码为类型约束：值具有源类型V t，而表达式具有源类型Z，因此类型静态地强制值的构造函数不能出现在期望表达式的地方，反之亦然。32L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23数据Vt数据ExpKFa，其中价值观KVnum：：Int->ExpKF（a（VInt））KVlam：：（a（Vs）-> a Z）->ExpKF（a（V（s->Z）KV对：：a（Vs）-> a（Vt）-> ExpKF（a（V（s，t）--表达式Klet_val：：a（Vt）->（a（Vt）-> a Z）->ExpKF（a Z）Klet_fst：： a（V（t1， t2））->（a（V t1）-> a Z）->ExpKF（a Z）Klet_snd：： a（V（t1，t2））->（a（Vt2）-> a Z）-> ExpKF（a Z）Klet_snd：： PrimOp -> a（VInt）-> a（VInt）->（a（VInt）-> a Z）->ExpKF（aZ）Kapp：： a（V（s-> Z））-> a（V s）->ExpKF（aZ）Kif0：： a（VInt）-> a Z -> a Z-> ExpKF（a Z）Khalt：： a（VInt）->ExpKF（a Z）类型ValKat= Rec ExpKF a（Vt）类型ExpKa= Rec ExpKF aZ图六、λK的有类型表示3.4证明类型对应在第一近似下，通过应用Curry-Howard同构，CPS变换的类型对应性（定理3.2）可以以这种方式反映在其实现的类型中cps：：（a. Expat）->（Exa.Val K a K t y p e t）- > Exp K a）->（Exa.Val K a K t y p e t）- > Exp Ka）->（Exa. 实验Ka）在这里，我们确实在Haskell类型表达式中使用K类型<$−）滥用了表示法-为了避免这个问题，我们对t和K类型（t）之间的对应性进行了证明。也就是说，我们改为键入cps如下：cps：：（西班牙a. Expat）-> cps_t. （CpsFormtcps_t，（图）（ValK a cps_t ->ExpKa）->ExpKa））其中，CpsForm t类型的值cpst表示cps t = Ktype<$t）的证明。这样的证明被编码在GADT中，GADT的数据构造器只允许在源语言的类型和CPS形式的对应类型之间创建有效的关联dataCpsFormt cps_twhereCpsInt：：CpsForm Int IntCpsPair：： CpsForms cps_s-> CpsFormtcps_t->CpsForm（s，t）（cps_s，cps_t）CpsFun：：CpsForms cps_s ->CpsFormt cps_t->CpsForm（s->t）（（cps_s，cps_t-> Z）-> Z）现在，由于我们使用了HOAS，我们必须稍微不同地构造CPS转换：我们将定义一个函数来执行单个节点的CPS转换2.2.）执行单个节点的CPS转换的函数的类型具有以下类型：cpsAux：：css. ExpF（CPS at）-> CPS at其中CPS a t表示源类型t的表达式的CPS转换形式，L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2333KK是一个缩写，其含义定义如下：类型CPSat=cps_t. （CpsFormtcps_t，（（ValK a cps_t ->ExpK a）->ExpK a））为了说明该技术，CPS转换对构造项（a，b）的情况如下实现：cpsAux（Pair（a：：CPS as）（b：：CPS at））=((s_cps_s，cps_a），（t_cps_t，cps_b））->（（CpsPair s_cps_st_cps_t），（λk ->（cps_a（λv1 -> cps_b（λv2 -> k（pairK v1v2）从这个例子中可以看出，代码遵循归纳证明的结构，其中CPS转换及其类型保持证明是交错的。最后，CPS改造的主要功能：cpsProg：：（cpsprog. Exp a t）->（Exp a t）ExpKa）通过将迭代器应用于函数cpsAux来获得。（因为它实现了Kprog−），所以它的类型不反映类型对应性，只反映类型保持。3.5函数依赖在类型对应证明的某些地方，我们需要使用λ→中给定类型的CPS形式是唯一的这一事实，即：定理3.3（CPS形式的唯一性）设K型（τ）=τK，K型（τ）=τJ，则τK=τJ。在[7]的意义上，我们把这一事实称为类型τ和它的CPS形式K（类型τ）之间的函数依赖。通过Curry-Howard同构，我们可以将这个定理编码为Haskell函数。首先，我们使用GADT编码类型相等data Equal a b whereEq_refl：： Equal a a其唯一的引入形式解释了反射性。定理3.3证明如下：cpsUnique：：CpsFormt cps_t ->CpsFormtcps_tcpsUnique（CpsFun（s_cps_s：： CpsForm s cps_s）（t_cps_t：：CpsFormtcps_t））（CpsFun（s_cps_s（t_cps_t= case cpsUnique s_cps_s s_cps_scase cpsUnique t_cps_t t_cps_tEq_refl例如，在函数应用的情况下，我们需要使用参数（e2）的CPS形式匹配34L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23CPS转换函数所期望的类型（e1）：cpsAux（App（e1：： CPS a（s->t））（e2：： CPS as）） =案例E1，（CpsFuns_cps_st_cps_t，m1）->（s_cps_s'，m 2）的情况e2case cps Eq_refl ->（t_cps（λk ->m1（λr1->m2（λr2 ->appKr1（pairK r2（contKk））4要点我们在这里讨论前一节和我们实际使用的代码之间的一些差异;我们的证明的不可靠性问题和我们试图解决它的方法;以及我们如何解决构造HOAS项的问题，我们现在已经方便地跳过了。4.1丹维和菲林斯基的CPS转换Danvy和Filinski与上述转换的本质区别反映在CPS转换项的表示中，在我们的设置中，转换项如下：类型CPSat=cps_t. （CpsFormtcps_t，（（ValK a cps_t->ExpK a）->ExpKa）， cps-meta（（ValK a（cps_t -> Z））->ExpK a））cps-obj也就是说，CPS中的项现在由（1）如前所述由元级延续参数化的项cps_meta和（2）由对象级延续参数化的项cps_obj（即，源类型的值（cpst->Z））表示。因此，一个术语的CPS转换同时定义了这两种形式。为了简化演示，我们在基本CPS转换的情况下处理了类型保持;我们的编译器实际上实现了Danvy和Filinski类型保持证明扩展到这种情况没有特别的困难。4.2（不）健全性我们的方法的一个问题是，类型保持证明是编码在一个不健全的逻辑。也就是说，可以将任何两个类型s和t之间的类型对应性的“证明”（即，CpsForm s t类型的值）作为非终止的Haskell项进行简单编码无论如何，编译器可以在事实发生后遍历类型保持证明，以验证它确实是完整的当然，在发展证明时，必须小心不要引入非终止性术语。然而，风险很小，这些条款的存在是L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2335这是相当明显的，而且考虑到我们正在编写证明的事实。也就是说，我们不是在PCC设置中，恶意对手利用我们逻辑的任何漏洞的可能性是首要考虑因素。在这里，证人的建构为此，我们相信我们的技术提供的置信度是合理的，尽管我们显然希望找到更好的东西。4.3Haskell类型类在采用不合理的逻辑操作显式证明之前，我们尝试了一种依赖于多参数类型类的其他方法。这种方法最初似乎更有前途和优雅。Haskell中类型类的预期用途是控制ad-hoc多态性。一个类型类可以被看作断言在该类型上定义的一组函数的存在的谓词，这些函数的实现作为实例声明的一部分提供。例如，Show类声明存在一个类型为t-> String的show函数，该函数定义为上课在Haskell 98标准中，一个类型类只能包含一个类型参数。然而，Haskell编译器支持的一个常见扩展允许定义多参数类型类，它将类型上的谓词的概念扩展到类型之间的关系因此，我们可以声明一个类型类来表示λ→中的类型和λK中的类型之间的关系：classCpsFormt cps_t并通过一组实例声明来定义关系：实例CpsFormInt Int实例（CpsForms cps_s，CpsFormtcps_t）=> CpsForm（s，t）（cps_s，cps_t）instance（CpsForms cps_s，CpsFormtcps_t）=> CpsForm（s ->t）（（cps_s，cps_t -> Z）-> Z）这些实例声明可以被视为（静态）类型级逻辑编程。每个实例声明都可以被理解为一个推理规则：第一个规则是一个公理，它声明了Int的CPS形式是Int，第二个规则声明了（s，t）的CPS形式是（cpss，cpst），前提是cpss是s的CPS形式，cpst是t的CPS形式，第三个规则也是如此。最后，我们可以表达这样一个事实，即关系是一个函数，它在类声明中有一个附加子句（函数依赖），如下所示：class CpsFormt cps_t |t-> cps_t现在，利用类型类，我们可以如下表示类型保持我们cpsAux：： ExpF（CPS at）-> CPS at但类型同义词CPS a t现在代表以下（存在）类型：36L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23类型CPSat=cps_t. cps表单tcps_t=>(ValK a cps_t ->ExpK a）->ExpK a不幸的是，在实践中，这个计划并没有让我们走得很远。GHC目前不能对这段代码进行类型检查，即使它在逻辑上看起来是正确的。要做到这一点，我们希望类型检查器应用函数依赖和实例声明来识别给定t的唯一类型cps t，并将此信息用作GADT类型细化的输入。但是目前GHC中还没有出现函数依赖和GADT之间的这种精确交互。这种情况可能会在未来发生变化，例如，如果在GHC中采用新的内部代表制[22]。值得注意的是，关联类型[1]可以提供一个有吸引力的替代函数依赖。但是，在缺乏关联类型的健壮实现的情况下，目前还不清楚我们是否会面临与类型类相同的4.4高阶项编译器前端执行词法和语法分析，并生成抽象语法树。这里，抽象语法树是高阶抽象语法中的术语。构造这种高阶项的有效表示是一些关注的主题。为了说明这一点，假设一个人试图构造一个直接产生高阶表示的解析器，那么他最终必然会编写一个本质上是这种形式的解析器解析 = case. 的... - > Lam（λx->. （parse x. ）... ）的情况下进行...问题是，被解析的函数体可能确实引用了新绑定的变量（x），因此该变量必须在递归调用中作为参数传递以进行解析。因此，生成的语法树在每个Lam节点下都包含一个解析调用，这对编译器的性能产生了巨大的影响幸运的是，这个问题有一个简单的解决方案。高阶表示可以通过元编程来构造，也就是说，通过使用Haskell的扩展，Haskell代码的片段可以在程序控制下进行操作。我们使用Template Haskell [20]，这是一种元编程工具，现在包含在GHC中。在我们的编译器中，我们使用一个解析器生成一阶抽象语法，然后使用Template Haskell将其转换为HOAS术语。一阶语法树以常规方式表示：数据AST，其中Fvar：： Ident ->ASTFlam：：Ident-> AST -> ASTFapp：： AST -> AST -> AST...其中Ident是标识符的类型我们定义了一个模板Haskell函数提升，L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）2337将此表示转换为HOAS：lift：：AST->ExpQ升力（Fvar x） = varE（mkNamex）升力（Flam xtb）=[|Lam$（lam1E（varP（mkNamex））（lift b））|]升力（Fapp a b）=[|应用程序$（电梯a）$（电梯b）|]...ExpQ类型是由Template Haskell定义的一种类型，用于表示Haskell表达式。语义括号（[|−|]）表示一个带引号的表达式，而$（−）形式用于从引号中转义（与Scheme的quasiquoteandunquote.）现在，我们可以用特殊形式$（lift ast）来应用上面的函数。因此，编译器的主函数遵循以下结构：compile：： ProgramText ->汇编编译program_text =letast=parse program_textexp= $（liftast）在（generate_code. 闭包转换。cps_conversion）exp本质上，lift重写了Haskell中的源程序，根据定义我们的HOAS表示的参数如果生成的Haskell代码是良好类型的，那么源程序也是良好类型的-5相关工作从TIL [23]和FLINT [17，16]开始，有很多关于类型化中间语言的工作，最初是由额外类型信息带来的优化机会所推动的[12]引入了携带证明码的思想，使得人们希望传播类型信息，甚至比早期的优化阶段更进一步，如[11]中所做的那样在[19]中，Shao et al.展示了一种低级类型化中间语言，用于编译器的后期阶段，对我们来说更重要的是，它们展示了如何编写CPS翻译，其类型保持属性是静态和机械验证的，就像我们的一样。在[13]中，Emir Pasalic开发了一个静态验证的类型安全解释器，用于具有绑定结构的语言，包括模式匹配。他使用的表示基于deBruijn索引，并依赖于Haskell中的类型相等在[2]中，Chiyan Chen等人也展示了一个CPS转换，其中类型保留属性被编码在Meta语言的类型系统中。他们以类似的方式使用GADT，包括显式地操纵证明，但他们也做了其他的设计权衡：他们的术语表示是使用deBruijn索引的一阶，他们的实现语言更具实验性。类似地，Linger和Sheard [10]在基于GADT的表示上使用deBruijn索引进行CPS变换;但与Chen和我们的工作相反，他们通过使用类型级别函数表示类型保持来避免对证明项的显式操作。38L- J. Guillemette，S.Monnier/Electronic Notes in Theoretical Computer Science 174（2007）23在[9]中，Leroy展示了用Coq证明助手编写的编译器的后端，并且其正确性证明是完全形式化的。他使用的语言的类型系统比我们的强大得多，但是他的计算语言 限制性更强在[5]中，Fegaras和Sheard展示了如何处理高阶抽象语法，在[24]中，Washburn和Weirich展示了如何在Haskell等语言中使用这种技术。我们使用后者的技术，并将其扩展到GADT和一元变质。GADT以许多不同的名称多次引入[25，3，21]。它们与类型类的相互作用是GHC中的一个已知问题，[22]中提出了一个可能的解决方案。6讨论和今后的工作HOAS的使用引起了对编译器性能的关注有一个问题是，它是否会导致大量的重复工作，就像我们没有使用Template Haskell的解析器一样。答案完全取决于编译器的结构：如果它被精简到每个中间表示只使用一次，那么性能不会提高太多。但是，在相同的中间表示上重复分析阶段显然会导致重复的工作。在这种情况下，我们当然，我们打算添加更多的编译阶段，如闭包转换，优化，寄存器分配，使其成为一个更现实的编译器。闭合转换尤其比CPS面临更大的挑战，因为它在w.r.t.程序分析 代码片段的类型（至少在局部，即在闭包中）取决于它的自由变量。这意味着一些程序分析必须静态地进行，以便在Haskell的类型系统中得到反映我们还打算通过添加参数多态和递归类型等特性来使源语言更加强大。我们还希望找到一些干净的方法来移动不健全的术语级的证明操作到健全的类型级。从长远来看，我们可能想研究如何生成PCC风格的证明。由于类型在编译期间不再真正传播，因此构建P