动态语言中异构序列的类型表示和计算

动态类型语言吉姆·牛顿引用此版本：吉姆·牛顿。动态类型语言中类型的表示和计算。符号计算[cs.SC]。索邦大学，2018年。英语。NNT：2018年SORUS440。电话：03018107HAL ID：电话：03018107https://theses.hal.science/tel-03018107提交日期：2020年HAL是一个多学科的开放存取档案馆，用于存放和传播科学研究论文，无论它们是否被公开。论文可以来自法国或国外的教学和研究机构，也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaireL’École Doctorale Informatique, Télécommunications et使用中的类型表示和计算动态类型语言扩展动态语言表达性以适应合理类型的序列向公众和杰出的评审团成员展示和辩护：记者Pr.波尔多大学/LaBRI/ UMR 5800记者博士帕斯卡尔·科斯坦萨·伊梅克评审团成员Barbara Jobstmann博士洛桑联邦理工学院（EPFL）评审团成员博士JeanBresson IRCAM/ CNRS/索邦大学评审团成员博士Chrisophe RhodesGoldsmiths伦敦大学校长Thierry GéraudEPITA/LRDE顾问Didier Verna EPITA博士/LRDE吉姆·爱德华·牛顿2018年11月20日摘要1PQP Q在本报告中，我们介绍了与异构序列的运行时类型检查相关的代码生成技术。传统的正则表达式[HMU06，YD14]可用于识别定义良好的字符串集，称为有理语言或有时称为正则语言。Newtonet al. [NDV16]提出了一种扩展，其中动态语言可以识别一组定义良好的异质序列，如列表和向量。与类比字符串匹配正则表达式理论一样，这些正则类型表达式的匹配也可以通过使用确定性有限自动机（FFA）来实现。构建这样的FFA可能会消耗时间。我们的方法使用元编程在编译时进行干预，高效地生成特定于每个FFA的函数，并允许编译器在可能的情况下进一步优化这些函数可在运行时使用。如果不使用这种元编程，程序可能会被迫在运行时构建FFA。这种构造的极高成本很可能会超过将字符串与表达式匹配所需的时间。我们的技术涉及通过deftype宏连接到Common Lisp类型系统。 编译器第一次遇到相关类型说明符时，会创建相应的FFA，可能是一个2n运算，从中生成特定的低级代码以匹配该特定表达式。此后，当再次遇到类型说明符时，可以使用相同的预生成函数。生成的代码在运行时的复杂度为{\displaystyle {n}}。我们在本报告中解释的这种方法的一个复杂之处是，为了构建FFA，我们必须计算一个消耗时间的不相交类型分解，这也导致了机器生成代码中类型酶的次优使用。为了处理复杂性，我们在机器生成的代码中使用了自己的优化类型酶宏。此宏的用法也会在编译时隐含扩充。我们的宏扩展使用二进制决策图（BDD）将优化的类型库优化为低级别代码，维护类型库语义，但消除冗余类型检查。在该报告中，我们还描述了BDD在Common Lisp类型系统中适应子类型的扩展，以及对BDD最坏情况大小的深入分析摘要2本文介绍了与异构但规则序列类型的动态验证相关的代码生成技术。我们将经典正则表达式通用化为类型正则表达式，调整它们的语法表面、内部表示、计算、优化和序列化（代码生成）。我们将基于S表达式的本机形式与二进制决策双图表示进行了比较，双图表示被丰富为在支持子类型的类型网格中表示布尔运算。然后，我们引入了最大不相交类型分解的概念，证明了这种分解的存在性和唯一性，并探索了计算这种分解的几种最大不相交类型分解用于处理表示类型正则表达式的确定性有限自动机。此自动机在编译时用于生成动态类型检查代码由此生成的代码先验地不考虑类型检查中可能因此，我们更详细地研究了这些问题，并再次使用二进制决策图理论来本文的工作重点是奉献3感谢Serge在过去12年中的爱和支持三年半前，他开玩笑地对我说："嫁给一个医生也不错。"没有他，我永远不会踏上这段旅程。这往往是令人兴奋的，有时是有压力的，但从来没有不可逾越的。这要归功于Serge，他一直是我的大力支持者。确认文件4我想向所有帮助我为这个博士项目做出贡献的人表示非常感谢Didier Verna和Theo Geraud给了我这个想法和机会去追求这个博士学位，他们多次挑战我的想法，导致更多的研究和更好地理解我的研究主题。从字面上讲，如果没有迪迪埃和西奥，这个博士项目就永远不可能完成。我谨向我的指导委员会Robert Strandh和Carlos Argon表示衷心的感谢，感谢他们在我每年的后续审查中提供的坦率反馈、宝贵的指导和洞察力。衷心感谢Pascal Costanza在这个博士项目中多次提供的帮助，感谢他在非常早期、混乱的阶段进行的讨论、评论文章，感谢他慷慨地同意成为我论文的官方评论员提前感谢所有尚未提及的评审团对我论文的宝贵反馈：Barbara Jobstmann、Christophe Rhodes和JeanBresson。我要感谢我在LRDE的所有同事，感谢他们以各种方式对我的研究项目做出的贡献：感谢ClémentDémoulins，感谢他对LRDE计算集群的所有帮助，如果没有这些帮助，我的计算将继续运行;感谢GuillaumeTochon，感谢他对许多统计学相关问题的耐心和热情的帮助;感谢Alexandre Duret-Lutz和MaximilienColange，感谢他们对我们的白板讨论，有时很愚蠢，但太多了，无法重复;感谢Akim Demaille，感谢他的技术投入，特别是在常规语言领域，这些语言已经被开发出来，对我的研究方向产生了重大影响。也感谢丹妮拉·贝克尔在法语和管理以及许多其他事情上的帮助，如果没有这些，我会失去这么多次，也感谢丹妮拉经常愿意倾听我的抱怨。感谢Priti Singh对手稿的出色校对，并在语法、清晰度、词汇和页面格式方面提出了许多更正建议。感 谢 几 位 帮 助 解 决 技 术 和 历 史 问 题 的 杰 出 人 士 ： Pascal Bourguignon 、 Lieven Marchand 、 BarryMargolin、Kent M.皮特曼、道格·卡茨曼和杰夫·巴内特。还要感谢Jean Éric Pin和Yann Régis-Gianas帮助我解决了几个技术问题。非常感谢Giuseppe Castagna多次帮助我获得视角，感谢我们的谈话和他的出版物，这些都是美妙和鼓舞人心的，也感谢他向我介绍Mariangiola Dezani，她愉快地为我提供了更有用的历史视角和背景。特别感谢Robert Strandh和Kathleen Callaway在过去三年中多次鼓励这个有趣而愉快的项目。内容物5Common Lisp11中的I正则序列1概述131.1导言131.2背景141.3类型化异源序列151.4有限自动机161.5优化的代码生成171.6二进制决策图191.7可用来源192通用Lisp类型系统202.1Common Lisp20中的类型2.2类型说明符的语义222.3有关类型的计算详细信息232.4子类型关系的无法回答的问题232.5类型说明符处理252.6使用s表达式的类型约简262.7功能类型272.7.1函数类型语义学272.7.2Common Lisp28中的函数类型2.7.3诱导子类型规则（ISR）292.7.4退化函数类型302.7.5功能类型交叉点322.7.6函数子类型关系的计算未明确说明332.7.7运行时类型的函数检查被认为是有害的2.7.8从历史的角度来看342.8相关工作342.9前景353理性语言373.1理性语言理论373.2正则表达式413.3正则表达式413.4有限自动机423.5有理表达式与有限自动机3.6有理表达式导数433.7使用有理导数机363.8相关工作474Common Lisp48中异构序列的类型检查4.1导言484.2Common Lisp49中的异构序列4.2.1正则表达式494.2.2澄清关于正则表达式的一些令人困惑的问题4.3应用用例534.3.1用例：基于RTP的字符串正则表达式4.3.2用例：基于可扩展序列的544.3.3使用案例：DWIM λ列表554.3.4使用案例：销毁案例574.4实施概述64内容物6||4.4.1模式匹配序列654.4.2类型定义654.4.3构造表示正则表达式的FFA 674.4.4优化的代码生成694.4.5粘性状态714.4.6重叠类型问题724.4.7满足的有理类型隐式表达式734.4.8已知开放式问题754.4.9RTE性能与手写代码774.4.10 RTE性能与CL-PPCRE774.4.11 特殊情况784.5备选方案：使用cons结构指定同质列表794.6相关工作814.7结论和观点81II二进制决策图835简化有序二进制决策图5.1BDD减少855.1.1初始构建步骤865.1.2减少规则885.2ROBDD布尔运算915.3ROBDD结构945.3.1通用Lisp ROBDD实现945.3.2BDD对象序列化和非序列化965.3.3通过哈希表98检索BDD5.4ROBDD布尔运算5.5具有多个参数的995.6生成n个变量1025.7结论和观点1046ROBDD105最坏情况的数值分析6.1最差情况ROBDD尺寸和形状1056.1.1过程总结1056.1.2最坏情况ROBDD106号的实验分析6.1.3ROBDD大小分布1066.1.4样本量112的充分性6.1.5测量ROBDD残余压缩1346.1.6最坏情况ROBDD136的形状6.1.7最差情况ROBDD尺寸1376.1.8阈值函数θ1406.1.9情节 ROBDDn及相关数量................................................................................................................ 1486.1.10 剩余压缩比的极限1496.2n变量ROBDD150最坏情况的程序化构造6.3相关工作1536.4结论1546.5前景1557扩展BSD以适应Common Lisp类型1567.1表示布尔表达式1567.2代表类型1567.3表示公共Lisp类型1577.4157年的今天7.4.1平等的权利和自由的孩子1577.4.2缓存BDD1577.4.3在存在亚型的情况下减少1577.4.4减少到儿童1587.4.5更复杂的关系类型1587.4.6优化的BDD结构15877.5相关工作1607.6前景160III类型分解和序列化问题1628最大不相交类型分解1648.1动机1658.2严格开发1668.2.1一元集合运算1668.2.2乐谱和封面1688.2.3西格玛代数1698.2.4有限数量的布尔组合1718.2.5不相交分解1788.2.6最大不相交分解1818.3相关工作1829计算MDTD1839.1基线设置不相交分解1849.2基线算法的微小改进1869.3作为SAT问题的类型不相交分解1889.4将不相交分解设置为图问题1899.4.1图形结构1919.4.2严格子集1949.4.3松弛子集1959.4.4触摸连接1969.4.5循环1989.4.6发现空集1999.4.7递归和迭代2029.5使用BDD203的类型分解9.5.1使用BDD204改进基线算法9.5.2使用BDD204改进基于图的算法9.6Baker子类型实现20510 MDTD算法的性能20610.2.9 游泳池：交叉点和工会21010.2.10 池：使用成员210的固定子类型10.3 MDTD算法实现21110.4 调整BDD哈希机制21110.5 调整基于BDD的图形算法21310.6 性能测试分析21810.7 Baker函数性能测试分析22010.8 剖面测试分析22210.9 按池224列出的MDTD算法的分析器图10.10按函数239列出的MDTD算法的分析器图10.11相关工作24910.12结论和观点24910.1测试概述。... ... ... ... ... ... ... ... ... ... ... ... ... ... . ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... 20610.2性能测试20710.2.1池：编号的子类型。... ... ... ... ... ... ... . ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... 20810.2.2池：条件的子类型。 . . . . ... . ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... 20810.2.3 池：数字或条件的子类型 . ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... 20910.2.4池：实数范围。... ... ... ... ... ... ... . ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ... 209811 类型酶优化策略25111.1 导言25111.2 类型规范方法25211.2.1 减少类型说明书25311.2.2 订单依赖性25411.2.3 相互分离的条款25511.2.4 启发式比较25611.2.5 通过自动重新订购25611.3 决策图方法25711.3.1 兼容类型规范257的ROBDD11.3.2 BDD结构符合型式规范26011.3.3 将BDD序列化为代码26111.3.4 发布编译器警告26211.4 相关工作26211.5 结论和观点26312 结论26512.1 捐款26512.2 第266章12.2.1 通用Lisp26612.2.2 异基因序列26612.2.3 二进制决策图26612.2.4 扩展BDD以适应Common Lisp类型26712.2.5 MDTD26712.2.6 优化Typecase26712.2.7 紧急问题268还原Lisp类型269的代码A.1基于定点的类型规范简化269A.2自下而上，功能样式，类型指定简化271B S表达式基线算法代码274C BDD基线算法275D 基于图的算法代码276D.1 图分解的支持代码276D.2 入口点功能276D.3 图形结构277D.4 断开节点277D.5 绿线功能278D.6 蓝箭函数278D.7 严格子集278D.8 松弛子集279D.9 触摸连接279D.10 第279章：一个女人D.11 基于S表达式的图形算法281D.12 基于BDD的图形算法282E 使用Clos283的函数子类F 在示例284上运行基于图的算法9ŤŮŞ命名法rn，ms整数区间表示法3.2，第37页。最坏情况ROBDD定义6.9的B带行索引，第136页。一元交集运算符。定义8.8，第167页一元联合运算符。定义8.7，第167页相互分离的结合。注释8.60，第180页。K格底记法2.6，第21页。Vr高度分布和定义n8.34，第172页。Δ2MHnpxq直方图差异e函数n定义于6.6，第113页。ǁ不相交关系集注释2.2，第20页。E鼠有理表达式注释3.22，第41页。他布尔公式变量密度。定义5.23，第100页。F分布式交集定义8.43，第174页。MHnpxq直方图样本m函数n符号6.3，第108页。Hnpxq直方图函数n定义n6.1，page106.Hnpxq归一化直方图m函数n定义n6.2，第108页。D分离性关闭定义8.33，第171页。C合取闭包定义8.32，第171页。rxs盖函数符号6.28，第143页。txu地板功能符号6.27，第143页。{ΔMHn}2L2直方图差函数的归一化符号6.7，第113页。理性语言符号3.20，第40页。不分离符号2.3，第20页。νprq可空定义3.26，第43页PpSqq tt的p空气符号6.41，第151页。BwL有理导数定义3.27，第44页。m2m个项目的顺序对编号符号6.12，第137页。φ概率分布函数注释6.5，第112页。PPPUQU的功率设置。定义8.11，第167页。psi实值阈值函数定义6.26，第143页。ρn残余压缩比定义6.8，第134页。10（c）Anri第k行的大小，自上而下的nRk k第k行的大小表达式生成的语言符号3.21，第41页。RBpVqSigma代数定义n9.1，page183.字母表定义3.1，第37页。⇒x所有有限长度单词的集合表示法3.8，第38页。⇒1单字母单词符号集3.7，第38页。σn直方图表示法给出的标准偏差6.4，第111页。nSk对行k'1到n中的节点求和定义6.14，第138页。严格子集或相等符号2.5，第21页。θ阈值函数定义6.25，第142页。J格顶记法2.7，第21页。|未归约有序BDD符号5.3的大小，第88页。|Size of unreduced ordered BDDNotation 5.3, page 88.**µ平均规范定义10.6，第214页。1平均L1规范定义10.7，第215页。{1}{2}{3}{4}{5}{6}{7}{8}{9}{10}{11}{12}{13}{14}{15}{16}{17}{18}{19}{20}{21}{22}{23}{24}{25}{26}{27}"独家黄金，对称差符号5.6，第91页。AB语言的连接定义3.12，第39页。AxKleene关闭语言A定义3.18，第40页。一种具有自身多个时态的语言。定义3.14，第39页。节点pqROBDD节点构造函数符号6.39，第151页。r'match a rational expression one or more times符号3.29，第45页B行行范围内的节点符号6.40，第151页。uv单词的连接定义3.10，第38页。Z学生分数定义10.9，第215页。AY函数类型定义2.16，第28页。一致一致的BDD节点定义5.5，第88页。FFA确定性有限自动机定义3.25，第42页。一组单词定义3.6，第38页。Lisp函数类型Lisp函数类型定义2.20，第29页。NDFA非确定性有限自动机定义3.24，第42页。有序BDD有序二进制决策图定义5.2，第87页。产品大小输入时间大小输出定义10.1，第206页。理性语言定义3.19，第40页。对称对称BDD节点定义5.4，第88页。Common Lisp类型定义2.1，第20页。type指定表示类型的对象。定义2.8，第21页。UOBDD未约化有序二进制决策图定义5.1，第86页。单词来自字母表的字符序列定义3.3，第37页。11第一部分Common Lisp12图1：我还没有考虑过我想写什么论文。这个博士研究项目着眼于一些现代动态编程语言中的一个特殊问题。许多现代编程语言支持允许序列是动态和异构的特性，这意味着内容的类型在运行时之前可能不是完全已知的，并且不同类型的对象可能包含在相同的序列中。我们提供了一种方法，使编译器可以使用一些信息，这些信息不是关于显式类型的，而是关于序列中类型的常规模式的。此外，这份报告描述了一个似乎有一个优雅的解决方案的问题，但当这个明显的解决方案被调查时，几个棘手的问题被揭示出来。提出了这些问题的解决方案，并分析了这些问题的一些性能方面在第一部分中，我们从第一章开始，对这个问题进行了高层次的概述在第4章中，我们将扩展CommonLisp类型系统以适应正则序列类型。在深入研究第4章之前，我们首先在第2章介绍了Common Lisp类型系统，在第3章介绍了有理语言。13P Q P Q第一章概述在本章中，我们总结了一种在Common Lisp中编写可识别异构类型序列的函数的技术该技术使用机器生成的序列识别函数，这些函数在编译时生成，并在运行时计算。我们演示的技术扩展了Common Lisp类型系统，利用了理性语言理论、BDD（二进制决策图）和图灵完成的Common Lisp宏工具。 最终的系统使用元编程将2n复杂度1运算从运行时移动到2n编译时运算，为运行时留下高度优化的n复杂度2运算我们请读者参考Wegener[Weg87，第1.5节]对Ω表示法的讨论1.1简介从出版物的数量来看，函数式编程似乎是一种越来越流行的趋势。关于函数式语言[Saj17，SGC15]和函数式编程[Cuk17，Wam11]。这种明显的增长可能是由于对分布式计算的需求函数范式提供了避免分布式算法中遇到的一些问题的工具。Scala Spark [KKWZ15]是一个用于实现大数据计算的强大而流行的功能接口的示例即使是非纯函数式语言也可以利用函数式范式。 Haveraen等人 [HMR '15]描述了函数式技术在高性能计算中的使用。Swaine [Swa17]在Clojure、Elixer、Scala、Swift和Lua等几种流行的脚本语言中说明了blant和微妙的函数属性。Hughes [Hug89]报告说，函数式语言提供的模块化使程序能够表达结果，而不是通过副作用t计算，从而消除了错误的来源函数式编程的介绍可以采用多种路径中的任何一种。对于一个季节性的Lisp程序来说，从看未类型的λ演算[Chu41，Pie02]开始理解基于评估的优雅模型是有意义的。Steele和Gabriel [SG93]认为Lisp语言比其他语言更关心表达性。然而，Lisp在一般情况下提供的表达能力与其在lambda演算中的子分支密切相关，即基于评估的模型和使用函数来表达计算的然而，为了处理更大的问题，程序员需要更多的抽象武器。Common Lisp[Ans94]编程语言提供了一个范例库，允许程序员在适当的时候使用函数式风格，还允许对象定向[BDG' 88，Kee89]、元对象编程[Pae93，KdRB91]、宏编程[Hoy08]和许多其他语言。函数式语言的学生遇到的另一种抽象是类型化λ演算形式的类型系统。编程语言中的类型为相应的语言带来了至少三种能力，在不同程度上取决于编程语言：（1）使编译器能够选择数据表示和优化[THFF' 17]，计算分配大小，和执行指针算术（类似于C语言[KR88]）（2）检测或消除某些程序员错误，如定义和调用站点之间的参数兼容性（如在逐步类型化[CL17]函数式语言和使用通用编程范例的C++[LGN12]中，LGN10]）允许程序员编写类型安全的程序，并允许编译器安全地进行某些优化，以及（3）允许程序员基于运行时数据的动态类型做出运行时决策。Common Lisp类型系统[Ans94，Section 4.2 Types]为编译器提供了内存分配和空间要求、检测某些类型的程序错误以及某些优化的信息。还可以利用类型系统根据信息类型做出运行时决策这种基于数据类型做出运行时决策的能力增加了程序的表达能力，并允许我们使用p2nq来表示复杂度的边界低于指数。[2]我们使用Θpnq来表示复杂度的上下边界是线性函数。14类型的概念将从结构区别扩展到语义区别。Castagna [CF05]报告说，将类型的概念扩展到语义区分，使得集合论能够在类型代数上使用。实际上，Common Lisp将类型简单地定义为一组对象。许多类型的运行时类型在执行速度方面检查incur惩罚无论如何，通过消除冗余计算或甚至在某些情况下将此类计算移动到编译时，可以减轻此类运行时决策的成本。在本研究中，我们利用了Common Lisp编程语言在序列类型方面的表达能力 本报告描述了当前的研究状态，包括将有理序列嵌入到Common Lisp类型系统、表面语法和转换为内部表示的问题的高层次观点。还讨论了与运行时类型检查计算相关的性能优化问题。一些昂贵的计算可以转移到编译时间。本文的重点是编译时间计算、证明算法的正确性、各种方法的性能测量以及不同数据结构的实验。这项工作将使Lisp程序员的小受众之外的大量用户随着函数式语言的日益普及，甚至出现了新的Lisp方言，如Clojure，Common Lisp的各种特性也在其他语言中得到了探索。当然，Common Lisp在历史上的许多独特优势来自于它的动态性质，现代语言试图在静态类型的语言中获得这种灵活性，而静态类型的语言有时被伪装成渐进类型的语言。Scala [OSV08，CB14]就是这种语言的一个例子。这种语言试图使类型声明在某些情况下是可选的，允许程序员编写在许多情况下看起来像动态语言的代码。编译器在需要的地方添加类型声明和断言，然后尝试完全删除运行时类型检查。我们认为，这些语言也可以从我们的一些工作成果中受益。最近，一些语言引入了元组类型（C++[Str13，Jos12]、Scala [OSV08，CB14]、Rust [Bla15]）。我们的工作为动态编程语言提供了类似的元组类型Shapeless [Che17]库允许Scala程序员通过异构列表利用类型级编程功能。我们还认为，随着在支持异构类型元组和序列的编程语言中完成更多的工作，特别是在也具有支持诸如联合和交集之类的理论运算集的类型系统的语言中[FCB08b，CF05]，自然会出现在这些序列中表达类型模式的需求。1.2背景Common Lisp是一种由其规范[Ans94]定义的编程语言，具有多种限制，包括开源和商业。对于本报告中解释的研究，我们使用SBCL [New15]作为选择实现所有实现都共享公共指定的功能性核心，并且每个实现都以各种方式扩展该功能我们利用的两个常见Lisp特性是它的宏系统和类型系统。下面是Common Lisp类型和宏的高级摘要Common Lisp宏系统[Gra96，Section 10.2]允许程序员编写编写代码的代码。宏可以使用defmacro定义，并且这样的宏通常在编译时扩展到编译后可在运行时执行的代码中。由于Common Lisp语言的同象性[McI60，Kay69]，宏采用Lisp对象的参数（符号、字符串、数字、列表等）。），并返回也是Lisp对象的程序片段编写宏的程序员可以在宏本身中使用语言的任何特征。有几个与Common Lisp宏相关的被很好地理解的警告。Costanza [CD10]探讨了这些卫生问题中最值得注意的问题。Costanza扩展了Clinger [CR91]的工作，Clinger声称Common Lisp存在一些问题，使其无法编写正常工作的宏。Common Lisp程序员了解这些困难和限制，通常编写宏，利用包系统和Gensym函数来避免名称冲突。Common Lisp类型系统[Ans94，Section 4]可以通过将类型视为对象集子类型对应于子集。超类型对应于超集。空类型（称为nil）对应于空集。该系统带有一些预定义的类型，如number、fixnum、rational等。此外，程序员可以编写类型说明符，这些说明符是根据其他类型进行的类型表达式的语法。这些类型旨在实现人机可读性。例如，（或数字字符串）表示数字集与字符串集的联接类似地，类型指定符可以分别使用运算符和、not、member和satisfies来进行合取、补集、枚举和谓词定义。Common Lisp允许类型用于变量和函数声明、对象中的插槽定义以及数组中的元素定义这些语句通常在程序编译期间考虑此外，Common Lisp还为基于类型的运行时反射提供了几个其他内置宏和函数。类型，类型酶，子类型，检查类型。程序员可以将新类型名称与composed相15示例1.2（与有理类型表达式关联的类型）。此示例与示例1.1完全类似。以字符串类型的对象开始，以符号类型的对象结束，并插入零个或多个（但有限多个）数字类型的对象。这样的序列包括像#（"hello"1 2 3 world）这样的向量和像（"hello"world）这样的列表，但不包括列表（34）。所有这样的序列的集合是由有理类型表达式pstringnumberx符号q标识的类型。有理数typeeexpressionpstringnumberxsymbolqdenoteseset（anddthusetype）offiniteesequences示例1.3（rte类型说明符的示例用法）。（defclassC（）（POINT：TYPE（ANDLST））（rte（：catnumbernumber）...））（defunF（XY））使用deftype的类型，其语法类似于defmacro的语法。1.3类型化异源序列虽然Common Lisp程序员可以为向量的所有元素指定同质类型[Ans 94，Section 15.1.2.2]，或者为列表的特定元素指定类型[Ans 94，System Class CONS]，但我们在本报告中解决的两个值得注意的限制是：1）没有为向量的不同元素指定异构类型的标准方法;2）没有为列表的所有元素声明类型（无论是异构的还是同质的）的标准方法。一个异构序列类型化模型的灵感来自Hopcroft [HMU06]提出的理性语言理论我们在第三章中正式定义的理性语言是一组有限序列，它们基本上遵循某种特定于语言的模式。正则表达式表征或指定该模式。示例1.1（表示理性语言的理性表达式） 有理表达式p bx c q定义以字符'a'开头、以字符'c'结尾并介于两者之间的所有字符序列的集合字符"b"出现零次或多次（但次数有限）这样的序列包括字符串"ac"、"bc"和"abbbbc"，但不是字符串"bc"所有这样的字符串的集合被称为p′bx′cq的有理语言。在像Common Lisp这样支持序列中对象的任意集合的编程语言中，我们可以很容易地认为这些对象的类型服从类似于有理表达式的模式。在第4章中讨论的一个有理类型表达式抽象地表示这样的序列中的类型模式。该概念被设计为对程序员直观，因为它类似于由正则表达式描述的模式。如第2章所述，Common Lisp语言将类型建模为集合。因此，我们可以认为理性语言不仅是集合，而且等价地是类型。正则表达式匹配字符根据字符相等性谓词组成字符串。相反，有理类型表达式通过元素类型成员资格谓词匹配序列的元素。有理表达式是由符号、超级脚本和中庸之道运算符组成的数学表达式。为了在Common Lisp编程语言中指定一个有理类型，我们借鉴了Lisp的传统，并定义了一个基于ASCII字符和前缀运算符的表面语法这个机器友好的基于S表达式的语法，我们称之为正则表达式类型。通过用用户定义的类型扩展类型系统，我们已经将正则表达式集成到了Common Lisp语言中（参见第4.4.2节）。我们已经通过deftype实现了一个名为rte（正则表达式）的参数化类型。rte的call-by-name参数是一个正则表达式，其语法在4.2.1节的图4.1中有详细说明。此类型的成员是与给定正则类型表达式匹配的所有序列16（declare（type（rte（：*（consnumber）（Y））...）（TYPECASEOBJECT（（rte（：*（：catt ttring（：*number）symbol）...）...））与所有用户定义的类型一样，rte类型可以在Common Lisp需要类型指定的任何地方使用。示例1.3说明了一些用例。C类的点槽被声明为正好有两个数字的列表。函数F需要一个参数Y，它是一个列表序列，其中每个列表都有一个数字作为它的第一个元素。1.4有限自动机编号符号图e1.1：有限te状态machine（DFA）（ofrationaltype表达式psymbolp数r'string'QQ'在1.3节中，我们对有理类型表达式进行了高层次的介绍，包括如何在Common Lisp程序中使用它们来为类型系统增加表达性。在本节中，我们将深入了解实施情况。该实现包括标准自动机理论的应用和几个感兴趣和具有挑战性的问题的发现。对这些问题的调查和提出的解决办法构成了本报告的主体。实现正则表达式的标准机制是有限自动机。解析曲面语法，即正则表达式，并将其转换为有限状态机。这项工作必须在程序中遇到的每个正则表达式一次完成，通常具有指数复杂度[Hro02]。因此，候选字符串可以通过简单地执行状态机以线性复杂度与正则表达式匹配在实现有理类型表达式时，我们遵循这种标准方法。Common Lisp友好的表面语法被转换成内部表示。如第3.6节所述，使用Brzozowski有理导数后的封闭建模技术，将该表示直接转换为确定性有限自动机（FFA）。我们偏离了Owens [OUT09a]提出的Brzozowski有理导数，因为潜在的重叠类型带来了挑战（见第4.4.6节）。为了确保自动机是确定性的，我们必须将正则类型表达式中提到的类型集分解为一个大的非相交类型集。这个问题被称为最大不相交类型分解（MDTD），并在第8章和第9章中讨论。编号2符号1字符串字符串符号3017示例1.4（生成的代码与正则表达式类型相匹配）。（LAMBDA（SEQUECE）（标签体）L0（when（nul llsequence））（returnil）;rejecting（optimized-typecase（popsequence）（symbol（goL1）（t（返回零））L1（when（nul llsequence））（returnil）;rejecting（optimized-typecase（popsequence）（number（goL2）（string（goL3））（t（returnnil））L2（when（nulllsequence））（RETTURNT）;ACCEPTING（optimized-typecase（popsequence）（number（goL2）（symbol（goL1））（t（返回零））L3（when（nulllsequence））（symbol（gol1））（t（返回零）示例1.5（复合Common Lisp类型说明符）。（或r（notnumber）（Eql 42）（andfixnum（notunsigned））（andunsigned（notfixnum）1.5优化的代码生成在运行时，确定给定序列与执行自动机的有理类型表达式量的匹配程度。有两种传统的方法可以做到这一点。第一种方法是具有将自动机和候选序列作为参数的通用匹配函数然后，函数执行自动机，就像它是一个虚拟机一样，指令来自候选序列。第二种方法是将自动机直接编译为目标体系结构上的代码，并在运行时执行该代码以匹配候选序列。在我们的例子中，我们将自动机编译成Common Lisp代码，并允许Common Lisp编译器生成特定于体系结构的代码。示例1.4显示了这样的Common Lisp代码可能的外观。关于这个函数的复杂性，需要注意的一点是，当这个函数应用于一个序列时，所遇到的状态数等于或小于序列中元素的数量因此，时间复杂度在序列的元素数上是线性的，并且与FFA中的状态数无关。由于我们能够在编译时间（或在某些情况下的加载时间）生成此代码，因此无论生成自动机的复杂性如何，运行时的复杂性都是线性的。在生成示例1.4中的代码时，我们处理了自动机中的每个状态。 每个状态都对应于结果代码中的标签。 每个标签都是对名为optimized-typecase的宏的调用，自动机中的每个转换都对应于optimized-typecase中