数据类型专门化中的幻影类型及递归模式

理论计算机科学电子笔记148（2006）211-237www.elsevier.com/locate/entcs具有幻影类型和递归模式的马修·弗卢特1里卡多·普切拉2康奈尔大学计算机科学系美国纽约州伊萨卡，邮编：14853摘要数据类型专门化是子类型化的一种形式，它捕获数据结构上的程序不变量，这些数据结构使用方便直观的数据类型表示法来表示。特别感兴趣的是结构不变量，如良构性。我们研究使用幻影类型来描述数据类型专门化。我们表明，它是可能的表示静态检查specializations内的类型系统的标准ML。我们还表明，这可以做到这一点的方式，不失去有用的编程设施，如模式匹配的情况下表达式。保留字：数据类型和结构，不变量1介绍在应用程序中普遍使用的数据结构通常具有一定程度的通用性，这使得它们适合（尽管并不总是很好地适合）它们的各种用途。这种通用性的一个好处是，它确保了数据结构的核心功能对所有客户端都可用。一个限制是，需要产生、消费或维护服从特定不变式的数据结构的实例的客户端难以强制执行该不变式。虽然许多语言都有一个类型系统，可以静态地对数据结构执行基本的安全属性，但很少有语言允许程序员直接在类型1Ema il：fluet@cs. C. C. C. N.E. L. e度2Ema il：ricca r do@cs. C. C. C. N.E.L. e度1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.046212M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211系统这是不幸的：当不变量被反射到类型系统中时，编译时类型错误将指示可能违反这些不变量的代码。为了使我们的讨论更具体，考虑布尔公式，我们在本文中使用它作为一个运行的例子。公式的直接表示如下：数据类型fmla =字符串变量|不是fmla| 真|和fmla的 * fmla| 假|或fmla * fmla的我们可以很容易地定义一个函数eval，它接受一个公式和一个将公式中的每个变量与真值相关联的环境，并返回公式的真值类似地，我们可以定义一个toString函数，它接受一个公式并返回该公式的字符串表示 众所周知，命题公式总是可以用一种特殊的形式表示，称为析取范式（或DNF），作为变量的合取和变量的否定的析取。DNF中的公式仍然是公式，但它它有一个受限的结构。一些运算公式的算法要求它们的输入以DNF表示;因此，静态检查公式是否在DNF中是有意义的。执行这种静态检查的一种方法是简单地为（通用）公式引入一种数据类型，为DNF公式引入另一种数据类型，并提供函数来显式地在它们之间进行转换当然，这是不明智的。例如，通过toString将DNF中的公式转换为字符串需要DNF公式的两次完整遍历（一次将其转换为通用一个用于构建字符串表示），以及分配中间结构（与原始公式大小相同）。另一种方法是将DNF公式定义为公式的特殊化。为了便于展示，我们假设专门化的特殊语法。这种语法应该是不言自明的：数据类型fmla =字符串变量|不是fmla| 真|和fmla的 * fmla| 假|或fmla * fmla的值，其中spec原子=字符串的变量和lit =字符串的变量|不是原子和conj = True|和lit * conj和dnf =假|或conj * dnf粗略地说，数据类型fmla的特殊化dnf受到限制，因此Or构造函数创建以False构造函数终止的合取列表合取由数据类型fmla的另一个专门化conj定义，它将And构造函数限制为形成文字列表。字面量本质上是一个变量或一个被否定的变量。这可以使用两种专门化来捕获，原子文字的atom和文字的lit通知M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211213为了定义dnf特化，我们需要所有的特化dnf、conj、lit和atom。这些特化导致了一个简单的子类型层次结构：FMLAssss、、利特斯Conj dnf原子对于一致性，我们认为数据类型是退化的专门化。从这个例子中抽象出来，我们将数据类型的专门化定义为由数据类型构造函数的子集生成的数据类型的版本，这些构造函数本身可能需要应用于数据类型的专门化。如果我们将数据类型的元素视为数据结构，那么我们可以将专门化的元素视为遵守某些限制的数据结构。数据类型的一组专门化可以以相互递归的方式指定。在本文中，我们展示了我们可以在标准ML [15]中实现人们对一种语言所期望的大部分内容，该语言具有直接支持上述专门化的类型系统。例如，我们可以编写一个toDnf函数，它不仅静态地保证其结果是一个公式，但它也是一个DNF公式。实施的好处在SML中使用专门化不变量的一个重要原因是，直接支持专门化的类型系统是复杂的，并且不是广泛可用的。（一个强制执行类似但严格来说更强大的不变量的类型系统是精化类型系统[3，8];见第4节。我们希望提供的专业化认证的关键特征是什么？首先，我们希望特殊类型的值的表示与原始数据类型的表示相同。这对于避免昂贵的运行时转换和允许代码重用非常重要。例如，我们应该能够实现一个函数，不仅计算一个未专门化的公式，而且计算任何专门化的公式，如dnf专业化此外，我们希望编写不包含在被检查值的专门化中未出现的构造函数的分支。例如，如果我们对一个具有特殊化dnf的值执行case分析，我们应该只需要为False和Or构造函数。借鉴以前关于幻影类型和子类型的工作[7]以及数据类型的专门化会导致子类型化的直觉，我们在第2节中提出了一个基于幻影类型的非正式翻译，从一组数据类型的专门化到一个接口，提供与专门化相对应的构造函数，析构函数和构造函数。该接口形成了一组最小的原语操作，214M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211专门化的功能（和静态保证）。它使用SML类型系统来实施由专门化体现的不变量。不幸的是，该接口还有很多需要改进的地方，特别是如果我们希望将数据类型专门化作为一种实用的编程技术，与标准的、惯用的SML用法自然集成。为了克服这些缺陷，特别是缺乏模式匹配，我们借鉴了另一种编程技术：递归方案[28]。我们在第3节中介绍了一个非正式的翻译，从一组数据类型的专门化，使用递归方案和上述接口，到一个改进的接口，通过真正的SML数据库提供专门化的功能。和前面一样，SML类型系统强制执行专门化的不变量。读者可能很想知道为什么我们选择在SML中编码专门化，而不是设计语言扩展。首先，有许多SML编译器[9，16，17，18，20，24，25];虽然这些编译器中的许多实现了一些语言扩展，但定义[15]所指定的SML语言在所有编译器中的行为都是相同的。因此，这里描述的技术现在对所有SML程序员都可用。 此外，在SML中编码专门化比编写我们自己的编译器或修改现有的编译器更方便。我们的数据类型专门化的概念是相当普遍的，我们相信它可以捕获大量有用的不变量。例如，我们可以定义一个特殊化，确保公式不包含变量：数据类型fmla =字符串变量|不是fmla| 真|和fmla的 * fmla| 假|或fmla * fmla，指定grnd=不属于grnd| 真|和grnd * grnd的| 假|或grnd * grnd以下专门化区分零和非零：数据类型nat= Zero |nat withspec zero=零的成功非零= nat的成功列表会导致有趣的专业化。考虑下面的特殊化，区分空列表、单例列表和非空列表：datatype'a list = Nil|'a * 'a listwithspec 'a empty = Nil的缺点而以下专门化区分偶数长度和奇数长度的列表：datatype' a l i s t= Nil|'a * 'a list的缺点M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211215其中spec 'a even = Nil|'a * 'a odd and 'a odd的缺点='a * 'a even的缺点最后，我们可以使用专门化来定义抽象语法树，以区分任意表达式和格式良好的表达式（例如，良好类型的表达式[4，13]，正规形式的表达式等）。下面是一个简单数据类型exp= Bool of bool|关于exp * exp| int的Int|加上exp * exp| 如果是exp * exp * expwithspec boolexp = Bool of bool|以及boolexp * boolexp| 如果boolexp * boolexp * boolexp且intexp=int的int|加上intexp * intexp| 如果是boolexp * intexp * intexp可以使用专门化来表达的更复杂的例子包括红黑树，它检查插入新元素后没有红色节点有红色子节点的关键不变量，以及简单类型λ演算中的表达式构造器，它只允许构建类型正确的表达式，本质上使用编码操作deBrujin索引。2具有虚拟类型的我们应该如何编写（在SML中）公式专门化的实现，以便类型系统强制执行适当的在本节中，我们将给出一个高度程式化的实现来实现这个特定的目标。我们希望读者能够理解这个实现对任意专门化的直接生成[3]我们认为，一个充分阐述的例子比正式的翻译更有指导意义，因为正式的翻译中的定义和符号变得繁琐和混乱。我们首先回顾幻影类型技术的本质及其在子类型化中的应用[7]。幻影类型技术使用类型等价的定义来将信息编码在一个类型的超连续类型变量中。（由于此类型变量的实例化对该类型值的运行时表示形式没有贡献，因此称为幻影类型。）然后，可以使用统一来对两个这样的类型所携带的信息强制执行特定的结构。当应用于子类型时，我们希望编码的信息是子类型层次结构中的位置。我们需要每个专业的编码σ-3我们的运行示例使用一阶单态数据类型，其抽象语法树木就是一个典型的例子。扩展实现来处理一阶多态数据库是很简单的。也可以处理更高阶的数据集;我们在第4节中简要地考虑这一点。216M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211这种编码应该在SML类型系统中产生一个类型，具有<$σ1与<$σ2<$<$统一的性质，当且仅当σ1是σ2在层次结构中的子类型（写作σ1≤σ2）。一个明显的问题是，我们想要使用统一（对称关系）来捕获子类型（非对称关系）。最简单的解决方案是使用两种编码：A·B·A定义为层级中的所有专业化。一个专门化σ的值将被赋予一个类型，使用<$σ<$C。 我们称之为具体的编码σ，我们假设它只使用接地类型（即，没有类型变量）。为了将操作或构造函数的域限制为作为特殊化σ的子类型的值的集合，我们使用σ的抽象编码<$σ<$A。为了让底层类型系统强制子类型层次结构，我们要求编码·C和·A通过满足以下属性来尊重对于所有的特殊化σ1和σ2，<$σ1<$C是唯一的，其中<$σ2<$Ai <$σ1≤σ2。为了允许统一，抽象编码引入了自由类型变量。由于在SML类型系统中，顶级类型不能包含自由类型变量，因此抽象编码总是某种多态类型方案的一部分。这导致了对抽象编码的使用的一些限制，其细节超出了本文的范围（但是，请参阅我们以前的工作[7]以获得全面的讨论）。我们断言抽象编码在下面的演示中使用得当。图1和图2给出了上述专门化的签名和相应实现。对于这样一个小例子来说，代码的数量可能看起来惊人，但我们将看到其中大部分是样板代码。 (In事实上，从专门化的声明性描述中机械地生成这段代码是很简单的;参见第5节。）而且，所有的动作都在签名！实现是微不足道的。这种代码爆炸的部分原因是我们将专门化概念上实现为具有显式构造函数和析构函数的抽象类型。（第3节展示了如何改进这个看似严厉的实现。）考虑到这一点，让我们研究一下签名的不同元素及其实现。类型签名的第一部分定义了公式专门化的类型。我们引入了一个多态类型第一系列的类型缩写将专门化的抽象编码与专门化类型结合起来，产生抽象类型。考虑类型ALit的定义：M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211217签名FMLA =签名（* specialization type*）type（* 抽象类型 *）type（* 混凝土类型 *）类型CFmla =单位AFmla类型CLit =单位ALit类型CAtom=单位AAtom类型CConj =单位AConj类型CDnf =单位ADnf结构Fmla：sig（* constructors*）valVar：string->CFmlavalNot：valTrue：CFmlavalAnd：val dest：真：unit->False：unit->：CFmla* CFmla->（* coercion *）val coerce：结构Lit： sigvalVar：string-> CLit valNot：val dest：端结构原子：签名valVar： string ->CAtomval dest：端结构Conj： sigvalTrue：CConjvalAnd：val dest：端结构Dnf：sigval False：CDnfval或 ：'a AConj * 'b ADnf->CDnfval dest：结束结束Fig. 1. FMLA签名type这里，{fmla：{lit：注意，记录标签的序列描述了从根到lit218M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211结构Fmla：>FMLA =结构Rep=结构（* 表示类型 *）数据类型t=字符串的变量|不是t| 真|和的t* t| 假|t*t的OR（*析构函数 *）funfail_ =raise匹配fun dest c（v，n，t，a，f，o）= Var（s）的情况c => v（s）|Not（f）=> n（f）| True =>t（）|并且（f，g）=> a（f，g）| False =>f（）|或者（f，g）=> o（f，g）（* pixels *）funcoerce（v）= v端（* specialization type *）type（* 抽象类型 *）type（* 混凝土类型 *）类型CFmla =单位AFmla类型CLit =单位ALit类型CAtom=单位AAtom类型CConj =单位AConj类型CDnf =单位ADnf结构Fmla =结构打开Repfun dest c {Var=v，Not=n，True=t，And=a，False=f，Or=o} = Rep.dest c（v，n，t，a，f，o） end结构Lit=结构打开Repfun dest c {Var=v，Not=n} = Rep.dest c（v，n，fail，fail，fail，fail） end结构原子=结构打开代表fun dest c {Var=v} = Rep.dest c（v，fail，fail，fail，fail，fail） end结构Conj=结构打开表示fun dest c {True=t，And=a} = Rep.dest c（fail，fail，t，a，fail，fail）端结构Dnf =结构打开表示fun dest c {False=f，Or=o}=代表目标c（失败，f，o）结束结束专业化4图二. FMLA结构第二系列的类型缩写实例化抽象类型[4]这本质上是我们以前的工作[7]中给出的树层次结构的编码。在该工作中给出的所有其他编码也适用于此M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211219与单元，产生具体类型。我们可以验证CLit和CAtom与ALit统一。我们还可以验证所有的具体类型都与AFmla统一起来，从而捕捉到fmla专门化是子类型层次结构的顶层元素这一事实。然而，CLit并不与AAtom、AConj或ADnf统一。换句话说，编码遵循子类型层次结构。在图2的实现中，我们看到类型Rep.t被实现为一个真正的SML数据类型，而类型子类型层次结构中位置的占位符。因此，所有的特殊化共享相同的表示。我们在图2中使用不透明签名匹配。 这对于获得幻象类型所需的行为至关重要。构造函数对于每个专门化，接口为专门化的每个构造函数提供一个函数。例如，atom专门化有一个构造函数（Var），因此我们提供了一个函数5val Atom.Var：string->CAtom它返回专门化原子的元素（因此是CAtom类型）。在适当的情况下，我们允许在构造函数参数上进行子类型化。因此，conj的And构造函数如下：val Conj.And：这些构造函数的实现很简单。它们只是表示类型的实际构造函数的别名（由open Rep带入范围）。将它们放置在不同的结构中可以让我们根据我们希望它们产生的专业化来限制它们的特定类型。销毁函数对于每个专门化，接口提供了一个析构函数，可以用来同时区分和解构专门化的元素，类似于SML中case表达式的操作方式。每个析构函数接受一个专门化元素以及应用于匹配构造函数参数的函数。作为一个例子，考虑Conj.dest，这是用于特殊化conj的析构函数。由于conj的元素仅使用True和And构造函数构建，因此解构这种专门化的元素可以5在下面和第3节中，我们偶尔会在签名或结构中使用长标识符来复制声明，其中SML语法需要一个（未限定的）标识符。我们这样做是为了明确表示代码的适当部分;在所有情况下，含义都应该是明确的。220M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211仅产生True构造函数或应用于lit值和conj值的And构造函数因此，我们给Conj.dest类型：val Conj.dest：和：CLit * CConj ->类似的推理允许我们删除或细化其他专门化的析构函数非正式地，当我们在协变类型位置使用具体编码和在逆变类型位置使用抽象编码时，特化的不变量被保留。这解释了分支函数的参数类型中析构函数也有一个简单的实现。它们只是作为SMLcase表达式实现。在没有提供函数的分支上，我们提出一个例外。如果特化是强制执行的，我们知道这些异常永远不会被引发！通过我们对子类型的编码，静态类型确保了这个异常永远不会被使用接口的程序引发[7]。强制转换最后，接口提供了将子类型转换为超类型的强制函数。这样的强制功能是必要的，因为直观地说，phantom类型只提供了一种受限的子类型化形式。为了说明这个问题，考虑以下函数;它不进行类型检查，因为真分支的类型是CLit，假分支的类型是CAtom-两种无法统一的：fun bad b =if b then Lit.Var（“p”） else Atom.Var（“q”）相反，我们必须写以下内容：fun good b =if b then Lit.Var（“p”）else Lit.coerce（Atom.Var（“q”））从技术上讲，这种行为是由于类型包容只发生在类型应用程序（在SML中是隐式的）上，而类型应用程序通常与函数应用程序一致因此，当不同专门化的两个表达式出现在必须具有相等类型的上下文中时，例如if表达式，则不会发生包含，并且必须强制一个共同的超类型。强制也有助于解决SML中排除使用多态递归的限制[10，11]。我们很快就会看到一个例子，说明这种强制的使用是必要的。强制函数的实现是微不足道的。它们只是改变值的（幻影）类型的标识函数M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）2112212.1示例让我们给出几个可以针对上面给出的公式专门化的接口编写的函数的例子。首先，考虑一个简单的函数来标识公式的顶级运算符fun identify（f：Var =fn_=>“变量”，Not =fn_ =>“求反”，True =fn_ =>“常量真”， And =fn_ =>“合取”，False=fn_=>“常量假”， Or =fn_ =>“析取”}请注意，identify的类型一个更有趣的例子是递归toString函数，它返回公式的字符串表示。下面是一个简单的实现funtoString（f：定义为f {Var= fns=>s，Not = fnf => concat["-"， toStringAnd =fn（f1，f2）=>concat["（“，toStringOr= fn（f1，f2）=> concat["（“，toString' f1，“|“，toString' f2，“）"]} in toString'（Fmla.coerce f）end请注意，toString但我们可以通过使用显式强制组合toString现在SML类型系统推断出toString函数所需的类型。如果我们有多态递归，我们可以直接将类型“a AFmla -> string to toString”赋给它人们可能会问，SML中缺乏多态递归是否会给专门化的使用正如我们所描述的。幸运的是，在合理的假设下，6可以证明专门化的使用从不需要多态递归。这是因为在专门化中使用phan- tom类型只会影响表达式或值的类型论证过程如下。考虑一个类型为σ-> τ的递归函数f，其特殊化为σ。f体中的任何递归调用都必须应用于6主要的假设是，在非专门化的数据类型上所需的递归函数本身可以在没有多态递归的情况下编写如果不是这样，那么函数无论是否有幻像类型和专门化，都不能用SML编写。(Thus，我们排除了非正则数据集的专门化。）另一方面，如果是这种情况，那么可以只使用专门化提供的接口来编写函数222M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211fun andConjs（f： CConj，g：CConj）：CConj =Conj.destf {True= fn（）=> g，And =fn（f1，f2）=> Conj.And（f1， andConjs（f2，g））} fun or Dnfs（f： CDnf，g：CDnf）：CDnf =Dnf.destf {False= fn（）=> g，或=fn（f1，f2）=> Dnf.或（f1，orDnfs（f2，g））} fun和ConjDnf（f： CConj，g：CDnf）：CDnf =Dnf.destg {False= fn（）=>Dnf.False，或=fn（g1，g2）=>Dnf。或（andConjs（f，g1），andConjDnf（f，g2））} fun和Dnfs（f：CDnf，g：CDnf）： CDnf =Dnf.dest f {False= fn（）=>Dnf.False，或者=fn（f1，f2）=>Dnf.dest g {False= fn（）=>Dnf.False，Or= fn（g1，g2）=> Dnf.Or（andConjs（f1，g1），或Dnfs（andConjDnf（f1，g2），或Dnfs（andConjDnf（g1，f2），（f2，g2）}}fun litToDnf（f：funtoDnfVar = fn s => litToDnf（Atom.Vars）， Not = fnf =>Fmla.destf {Var= fn s=> litToDnf（Lit.Not（Atom.Vars））， Not= fnf=> toDnfTrue= fn（）=> toDnfAnd = fn（f，g） => toDnf或=fn（f，g）=> toDnfAnd =fn（f，g）=>andDnfs（toDnf或者=fn（f，g）=>orDnfs（toDnf图三. toDnf函数特殊化σJ，其中σJ是σ的子类型。因为σJ是σ的一个子类型，所以存在从σJ到σ的强制转换。 因此，我们总是可以实现函数 正如我们对toString函数所做的那样：将辅助函数f'的域设置为σ的具体编码，并将递归调用写成f'（σ.coerce x）。（在toString示例中，所有递归调用都针对CFmla类型的值，因此可以省略强制转换。）最后，我们通过将f'与σ.coerce组合来恢复f的自变量中的适当子类型。图3给出了一个扩展示例，最终使用toDnf函数将任何公式转换为等效的DNF公式。此函数的类型'我们进一步注意到，图3中类型注释的使用完全超级棒 类型推理将精确地推导出这些类型。在SML类型系统所作的保证和使用幻影类型技术的专门化库所作的保证之间存在着差异。虽然前者确保M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211223如果专门化库被正确地实现，则后者确保“良好类型的我们希望本节已经说明了专门化库的实现是简单的。然而，更微妙的一点是，为了获得额外的静态保证的好处，必须选择捕获感兴趣的属性和不变量的特殊化3使用递归方案的虽然第2节描述了一个有趣的理论结果--定义一个toDnf函数的能力，该函数的类型静态地强制一个结构不变，而不依赖于单独的数据集--但目前还不清楚所提出的方法是否在实践中可用。特别是，对特殊化类型的模式匹配必须通过应用析构函数来执行，而不是通过SML的结果是图3中的尽管模式匹配的任何使用都可以在析构函数的应用程序中去除，但模式匹配编程习惯的重要方面受到前一节中编码的严重抑制。检查图3可以发现两个特别明显的可读性问题，可以通过模式匹配来改进。首先，考虑andDnfs函数。非正式地，可以用以下方式描述函数的预期行为：考虑dnf专门化中的两个参数：如果其中一个参数是False元素，则返回False;如果两个参数都是Or元素，则返回元素参数的成对合取的析取。不幸的是，编写的代码掩盖了这种行为。这突出了模式匹配中缺少的两个方面：通过元组模式中嵌套数据类型模式来同时匹配的能力，以及给出通配符匹配的能力。其次，考虑toDnf在这里，人们错过了能力，编写嵌套模式，这将把析构函数的两个应用程序组合成一个模式匹配。为了进行比较，图4为未特殊化的Rep.t数据类型实现了toDnf函数，解决了上述问题然而，这一明显改进是有代价的。编译器现在会发出多个nonex-haustive匹配警告。更重要的是，类型系统不能保证结果是析取范式。7 感谢一位匿名评论者224M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211fun andConjs（f： Rep.t，g：Rep.t）：Rep.t= casef of Rep.True=> g|Rep.And（f1，f2）=> Rep.And（f1，andConjs（f2，g））fun or Dnfs（f：Rep.t，g：Rep.t）：Rep.t =假设f为假=> g| Rep.Or（f1，f2）=>Rep.Or（f1，orDnfs（f2，g））fun and ConjDnf（f：Rep.t，g：Rep.t）：Rep.t =假设g => Rep.False| Rep.Or（g1，g2）=>Rep.Or（andConjs（f，g1），andConjDnf（f，g2））fun andDnfs（f：Rep.t，g：Rep.t）：Rep.t =例（f，g）（Rep.False，_）=> Rep.False| （_，Rep.False）=> Rep.False|（Rep.Or（f1，f2），Rep.Or（g1，g2））=> Rep.Or（andConjs（f1，g1），或Dnfs（andConjDnf（f1，g2），或Dnfs（andConjDnf（g1，f2），和Dnfs（f2， g2）fun litToDnf（f： Rep.t）：Rep.t= Rep.或（Rep.And（f，Rep.True），Rep.False）fun toDnf（f： Rep.t）：Rep.t=letfunto DnfRep.Var s => litToDnf（Rep.Var s）| Rep.Not（Rep.Vars）=> litToDnf（Rep.Not（Rep.Var s））| Rep.Not（Rep.Notf）=> toDnf 'f| Rep.Not Rep.True =>Rep.False|Rep.Not（Rep.And（f，g））=> toDnf ' （ R e p . O r （ R e p . N o t f ， R e p . N o t g ） ）| Rep.Not Rep.False => toDnf ' Rep. True| Rep.Not（Rep.Or（f，g））=>toDnf'（Rep.And（Rep.Not f，Rep.Not g））| Rep.True => Rep.Or（Rep.True，Rep.False）| Rep.And（f，g）=> andDnfs（toDnf' f ， t o D n f ' g ）| Rep.False =>Rep.False| Rep.Or (f,g) => orDnfs (toDnf’ f, toDnf’ g)in toDnf’ f end见图4。toDnf函数（通过非专用化的Rep.t数据类型）我们寻求一种解决方案，将模式匹配的表达性和方便性回想一下我们在引言中所做的观察：通过为每个专门化使用不同的数据库并提供在它们之间转换的函数，正如我们所指出的，这是不合理的。然而，有一个中间的解决方案，一个使用不同的datashees为他们的诱导模式和细粒度的datasheons本地化datashees到和从专门化类型和专门化datashees。我们以Wang和Murphy的递归方案为灵感利用两级类型，将归纳定义的类型分为表示类型结构的组件和连接递归结的组件，递归模式提供了一种编程习惯，可以隐藏抽象类型的表示，同时仍然支持模式匹配。粗略地说，该技术建议为每个专业化定义一个数据类型，它代表专业化的顶层结构。专门化的模式匹配是通过首先转换M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211225签名FMLA_DT =sig包括FMLA结构Fmla：sig（* specialization datatype *）datatype（'not，' andl，'andr，' orl，'orr）t' = Var' of string|不是' of 'not|和' of 'andl * 'andr |And’ of ’andl*’andr|或者“of”orl *“orr |Or’of’orl *’orr（* 注射 *）val inj：val prj：valmap：（（'not1-> 'not2）*(’andl1 -> ’andl2) * (’andr1 -> ’andr2) *(’orll1 -> ’orll2) * (’orr1 -> ’orr2))（'not1，'andl1，'andr1，'orll1，'orr1）t（'not2，'andl2，'andr2，'orll2，'orr2）t'端结构Lit： sig字符串的数据类型“not t”= Var“|Not ' of'not val inj：'a AAtom t' -> CLitvalprj：valmap：结构原子：签名datatypetval prj：端结构Conj： sigdatatype（'andl，'andr）t' = True' |And 'of'andl*'andrvalinj：（'aALit，'bAConj）t'->CConjval prj：valmap：（（'andl1-> 'andl2）*（'andr1-> 'andr2））->(’andl1,’andr1) t’ -> (’andl2,’andr2)端结构Dnf：sigdatatype（'orll，'orr）t' = False'|Or ' of 'o rll * 'o rr valinj ： （' a AC on j， 'b AD nf ） t' -> CDnfval prj：valmap：（（'orll1，' orr1）t'->(’orll2,’orr2)端（* 特殊化数据类型类型 *）type类型DAtom = Atom.t'type端图五. FMLADT签名8专门化为适当的数据类型，然后匹配结果。重要的一点是，我们不需要将整个专门化转换为专门化数据类型，而只是需要执行模式匹配。226M. 弗卢埃特河Pucella/Electronic Notes in Theoretical Computer Science 148（2006）211结构FmlaDT：FMLA_DT =结构打开Fmla结构Fmla =结构打开Fmla（* specialization datatype *）datatype（'not，' andl，'andr，' orl，'orr）t' = Var' of string|不是' of'not|和' of 'andl * 'andr |And’ of ’andl*’andr|或者“of”orl *“orr |Or’of’orl *’orr（* injection*）fun inj f=Var s的情况f => Var s|不' f =>不f|And '（f1，f2）=> And（f1，f2）|And’ (f1, f2) => And (f1, f2)| False' =>False|Or'（f1，f2）=> Or（f1，f2）（* projection *）funprj f =dest f{Var =Var'，Not = Not'，True = fn（） =>（*地图*）有趣的地图（F1，F2，F3，F4，F5）f=Var's的情况f => Var 's|Not ' f = > N o t ' （ F 1 f ）|And'（f1，f2）=> And'（F2 f1，F3 f2）|And’ (f1, f2) => And’ (F2 f1, F3 f2)|或'（f1，f2）=>或'（F4 f1，F5 f2）|Or’ (f1,f2) => Or’ (F4 f1, F5 f2)端结构Lit=结构打开Lit字符串的数据类型“not t”= Var“|不是' of 'notfun inj f= Var' s的情况f=> Var's |Not' f => Not f fun prj f =dest f {Var = Var'，Not = Not'}有趣的映射F f = Var's的情况f => Var 's|Not ' f => Not'（F f）end结构原子=结构开放原子字符串的数据类型tfuninj f= casef ofVarFunmapf=Var's的casef结构Conj=结构打开Conjdatatype（'andl，'andr）t' = True'|和'o f' a n d l*' andrfun injf=casefof True' => True|And' （ f 1 ， f 2 ） = > A n d （ f 1 ， f 2 ）f u n p r j f