嵌入式领域专用语言的类型系统：Haskell的案例研究与评估

233理论计算机科学电子笔记76（2002）网址：http://www.elsevier.nl/locate/entcs/volume76.html19页领域专用语言的可编程类型系统Peter Thiemann彼得·蒂曼1，2InstitutfuürInformatikUniversitüatFreiburgGeorges-Koühller-Allee079D-79110 Freiburg，Germany摘要具有可编程类型系统的语言对于构建嵌入式领域专用语言（EDSL）至关重要。驱动的EDSL服务器端Web脚本的实现所提出的要求，我们检查两个主要的扩展类型系统的主机语言，Haskell。 我们表明，一个组件，确保正确的HTML文档的生成可以很好地利用类型级的功能，实现使用功能逻辑重载。我们进一步表明，一个函数，确保提交给Web脚本的数据与脚本所期望的数据的一致性是不那么尴尬在类型语言中存在lambda表达式时使用。 在这两种情况下，我们评估了使用类型获得的保证，并探索替代解决方案。1介绍领域特定语言（DSL）正在解决特定领域的编程需求它们旨在根据领域本身的概念来处理和解决领域中的问题因此，它们可以提高领域专家的生产力，而这些领域专家不需要是编程专家。由于DSL的用户群有限，因此必须根据用户的生产率收益来仔细权衡其开发和实现所因此，实现DSL的一种流行方法特别是，函数式编程语言已被证明是很好的宿主语言，因为它们具有正交抽象功能，1电邮地址：thiemann@informatik.uni-freiburg.de2这项工作是在俄勒冈健康科学大学逗留期间完成的，由SwagenStiftung。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。T·希曼234先进的类型系统。嵌入方法的另一个优点是，DSL很容易扩展和定制到特定的然而，事实证明，类型系统是一种资产，同时也是一个缺点。虽然可以用类型语言表达许多领域概念，但最终的类型通常很不自然- 某些类型的要求甚至强制使用特定的编程风格。这种在这一点上，领域专家需要一个编程语言专家来破译编译器的话语。因此，我们正在努力寻找更好的方法，在函数式编程语言Haskell的上下文中将域概念集成到类型语言中。首先，我们开发了一个激励性的例子，它来自于用于Web脚本的DSL[16，17，18]。在这个例子的指导下，我们展示了一种扩展类型语言的可行方法是在类型级别安装（一阶）函数逻辑编程语言[4]。其思想是，在类型级别的术语重写系统捕获特定于域的概念和函数逻辑编程的执行机制（例如，缩小或剩余）是类型推理过程的基础。理想情况下，在类型级别的术语重写系统的语义与在值级别的编程语言的语义一致，从而允许将值级别函数提升到类型级别而不改变它们的语义。基本理论建立在HM（X）类型推理框架上[15]。下一步是在类型级别添加lambda表达式[13]。这一步骤同样是由应用程序领域的实际需求驱动的，我们希望用最简单和最自然的方式来表达问题。我们展示了一个问题，其基于Haskell98的解决方案导致扭曲的程序，很难解释和理解。接下来，我们讨论另一种在类型语言中使用lambda抽象的解决方案。它会导致相当自然的程序。我们进一步探讨了一个替代的API的激励的例子，并表明，它也需要通用编程设施。最后，我们评估了通过类型化实现的属性，并使用秩2类型对它们进行了细化。在本文中，我们假设熟悉函数式编程语言Haskell [8]。2洗WASH（Web Application Services in Haskell）是一个用于设计和实现Web服务的领域特定语言的集合每种语言都嵌入在Haskell中，并以Haskell库的形式提供这个想法是，这些语言可以根据开发中的应用程序的需要进行混合和匹配T·希曼235WASH的两个重要部分是WASH/HTML和WASH/CGI。第一部分，WASH/HTML，[16]处理HTML和XML文档的生成，而WASH/CGI [17]为服务器端Web脚本提供了方便的API。WASH/HTML的显著特点是，用WASH/HTML编程的文档生成器保证只生成格式良好的HTML页面，并且在很大程度上也是有效的HTML页面，前提是生成器程序本身是类型正确的。WASH/CGI通过隐藏浏览器和服务器之间通信的大部分繁琐细节，为服务器端Web脚本提供了一个简单的基于回调的它还使用类型系统来保证浏览器提交的表单与处理这些表单的程序之间的一致性3类型检查HTML生成器在本节中，我们考虑的问题是，仅通过对程序进行类型检查就能保证程序在讨论了WASH/HTML的发布版本的设计之后，我们考虑了一个更容易适应的解决方案，该解决方案在很大程度上依赖于在编译时在类型检查器中进行的计算。大多数Web页面都是由运行在Web服务器上的脚本在Web服务器上生成的这是一个公认的问题，这些网页往往违反了W3C标准的XHTML [19]。该标准要求文档格式良好，并且根据XHTML文档类型定义（DTD）有效在一个格式良好的文档中，开始和结束标记被正确地嵌套，这样文档就实际上是一个标记和属性树的可重复呈现。这种树中的主要节点称为元素，元素的标签提供了它的名称，该名称反映在开始和结束标记中。有效性表明满足DTD施加的限制。DTD基本上将每个元素名称与元素名称上的正则表达式相关联如果对于每个名为N的元素，N的子元素的名称序列被DTD关联到N的正则表达式接受，则格式良好的文档是有效的例如，XHTML的DTD规定，名为dl的元素只能有一个名为dt或dd的非空元素序列作为子元素。<！ELEMENTdl（dt| dd）+>3.1保证格式良好许多生成的Web页面甚至不是格式良好的主要原因是使用了不适当的编程接口来生成它们。通常，页面是由print语句序列生成的。因此，程序员很容易失去对打开标记堆栈的跟踪因此，他T·希曼236可以关闭根本没有打开的元素，或者被后来打开但尚未关闭的其他元素遮挡的元素。我们避免这些问题的方法是首先构建文档的内部树表示。只有在构建了整个文档树之后，文档的一次遍历才能将其序列化为XHTML syn- tax。因此，生成器库必须提供构建该内部树的操作WASH/HTML为每个元素提供了一个组合子（一个Haskell函数），它与元素同名。combinator并不简单地构建新元素。相反，它通过在子元素序列的末尾附加新元素来转换现有（父）元素同样，它不仅接受子元素序列，而且接受一个可以添加子元素和属性的Transformer函数作为一个例子，我们展示了一个元素组合子的初步类型dt：：（元素->元素）->（元素->元素）参数函数通过附加子元素和属性来转换dt元素，而结果函数是将dt元素添加到父元素的Transformer这种方法具有吸引力，原因有很多。首先，所有类型的节点、元素和属性都可以被统一处理其次，我们通过组合转换函数，免费获得了“元素和属性序列”的概念3.2保证有效性为了保证有效性，我们建议增强元素组合器的类型由于我们需要跟踪元素名来检查有效性，因此第一步是使元素名在类型级别可用为此，库为每个元素名称提供了一个同名的数据类型（受名称修改的影响，以解决Haskell强加的例如，dt标记的类型是DT，其定义如下。数据DT = DT这种数据类型只有一个可观察值，即DT。3因此，我们通常称这些类型为单例类型，因为这种类型在类型理论中被称为现在的想法是通过范围覆盖单例类型的幻影类型来参数化Element类型这产生了dt组合子的另一种潜在类型dt：：（元素DT->元素DT）->（Element parent-> Element parent）3标识符DT一次用作左侧的类型名称，一次用作右侧的数据常量名称。T·希曼237||有了这种类型，还有两件事要做。首先，父类型不应该是任意的。由于DTD只允许dt元素作为dl元素的子元素，我们可能想用DL替换parent。然而，这种方法一般不起作用，因为可能存在许多不同的可接受父元素。幸运的是，这种限制可以使用标准Haskell类型类进行建模。对于每个元素名N，我们引入一个类型类，它恰好包含那些允许名为N的子元素的元素类型的集合。4例如，dt元素产生类class AdmitChildDT parent其中dt：：（元素DT->元素DT）->（Element parent-> Element parent）实例AdmitChildDT DL在这个例子中，只有一个实例（即，只有一个元素名允许dt元素作为其子元素），但一般来说，可能有多达50个元素名可用于父元素。在这里停下来并将这种类型用于只有部分有效性保证的API是非常有意义的。这种类型已经排除了大多数错误，因为XHTMLDTD中的许多正则表达式都具有（N1.这正是AdmitChild类型类实现的。此外，进一步加强类型约束使得图书馆很难使用。其次，子元素的顺序也不能是任意的。将注意力转移回dl元素，其中子元素必须形成dd和dt元素的非空序列，类型必须防止将空dl元素添加到其父元素中的尝试。在库中，当它被实现时[16]，我们采取以下方法。对于每个XHTML元素名称，我们通过使用标准技术从DTD编译其相关的正则表达式来构造有限自动机[1]。Element类型接收另一个phantom类型参数，该参数的范围涵盖了此类有限自动机的状态。因此，dt组合子的类型被定义为：类AdmitChildDT父级，其中dt：：（FinalStateDT state，DeltaDT parent pstate=>（元素DT状态0->元素DT状态）->（Element parent pstate-> Element parent在该类型中，FinalStateDT是一个Haskell类型类，它描述了与DT相关的自动机的最终状态集。然而，实现自动机的转换功能的DeltaDT父pstatepstate4这简化了WASH/HTML的早期版本，该版本需要一个双参数类型类[16]。T·希曼238\{|∈}是一个三参数类型类的应用程序，一个广泛实现的Haskell扩展，其中parent是父元素的名称，pstate是读取DT之前父元素的自动机的状态类型STATE0代表与元素dt相关联的自动机的初始状态。为了避免二义性问题，使用另一个Haskell扩展，函数依赖是有利的[11]。简单地说，声明DeltaDT的函数依赖父级pstate-> pstate '允许类型检查器将DeltaDT视为将父级和pstate映射到pstate'的函数。虽然这种方法是可行的，但它表现出许多缺点。特别是，一旦DTD被编译成AdmitChild类和转换函数的库，就很难在Java上扩展该库因此，该解决方案不是非常灵活的。另一个要点是在功能性表述更容易理解的地方3.3函数逻辑重载因此，我们建议使用函数逻辑重载对转换函数进行编码[4]。这个框架的主要思想是允许在类型中使用函数，并让类型推理引擎在编译时处理这些函数的求值。由于在类型推理过程中存在于类型中的变量是逻辑变量，这将类型推理引擎置于函数逻辑编程的设置中[6]。这反过来又使得在类型检查器的实现中能够使用函数逻辑编程语言[7]使用这种方法，我们进行如下。我们没有将正则表达式预编译为有限自动机并将它们硬编码在类型结构中，而是采用正则表达式的导数的想法[2]来避免显式构造有限自动机。Brzozowski [2]表明，从正则表达式r和输入符号a开始，可以计算另一个正则表达式d（r，a）（r的a-导数），使得L（d（r，a））=a L（r）=w aw L（r）。 迭代这个构造会产生一组有限的正则表达式，这些正则表达式在求导下是封闭的这个集合可以被看作是一个有限自动机的状态集合，其中d是它的转移函数。最终状态是那些识别空单词的正则表达式。编写函数d和函数e来检查正则表达式是否识别Haskell中的空单词是一个简单的练习。然而，将这种实现提升到类型级别的函数是一项非常复杂的任务，特别是在手头只有多参数类型类和函数依赖的情况下[14]。例如，一个简单的两行equals函数的输入符号定义在类型级别上有一个令人惊讶的笨拙然而，使用函数逻辑重载，代码不需要重写，但两行定义可以在类型级别上重用。T·希曼239执行引擎保证代码在类型级别的语义与值级别的语义相同作为一个例子，我们看一下dl类型的各个版本，其中涉及正则表达式（dt|（dd）+。后者被编码为（PLUS（UNION（ATOM DT）（ATOMDD），其中PLUS是对应于+运算符的类型构造函数，UNION对应于|运算符，ATOM将字母表的元素映射到正则表达式。class AdmitChildDL parent其中dl：：（AcceptsEmptyWord状态）=>（元素DL（PLUS（UNION（ATOM DT）（ATOM DD）->元素DL状态）->（元素父级pstate->元素父元素（Delta pstate DL））由于从关系的观点转变为功能的观点，虚假的pstate'变量消失了此外，Delta不再依赖于parent，因为正则表达式pstate包含所有必要的信息。54类型检查Web浏览器Web应用程序的开发人员面临着许多问题。由于底层HTTP协议的无状态性质，应用程序通常必须被拆分为许多脚本，其中每个脚本对应于与用户交互的一个或因此，开发人员必须确保没有悬空的交互，这意味着每当用户向Web服务器提交一个答案（所谓的表单）时，服务器上就会安装一个这个属性非常脆弱，它可能会被意外重命名或删除脚本或不正确的安装所破坏此外，提交的表单必须至少包含脚本希望处理的信息，即：如果一个脚本在表单中要求一个特定的字段，那么这个字段应该存在。WASH/CGI库确保了这两个要求。首先，整个交互可以作为一个单独的程序进行编程，也可以这样安装WASH/CGI库自动跟踪交互的状态，而不需要程序员的注意。相反，程序员只是将回调动作附加到表单的提交按钮上，以指定应用程序内部的控制流程因此，完全避免了危险相互作用的问题 第 二 ， 表 单 的 字 段 在 WASH/CGI 脚 本 中 从 不 被 名 称 相 反 ， 每 当WASH/CGI脚本创建一个输入字段时，它都会获得该字段的类型化句柄最初，句柄是无效的，即，则无法提取其值。 则5 公平地说，这种依赖性也可以在关系情况下被移除，把父母的名字写进州里。T·希曼240句柄通过提交机制传递给回调操作。提交机制对句柄进行类型修改，拒绝不正确或其他形式错误的表单提交，并在检测到错误时让用户重复提交在检查句柄之后，提交机制将一个经过验证的句柄传递给回调操作。回调操作现在可以当然，可以以这种方式一次处理多个在下文中，我们将深入研究验证子任务的机制首先，我们讨论标准的Haskell 98解决方案，因为它是在WASH/CGI中实现的。其次，我们展示了一种替代解决方案，通过避免Haskell98解决方案的一些不便之处来改进它第三，我们考虑进一步可能的打字提交功能，并讨论其优点。最后，我们评估整个验证机制。4.1使用Haskell98进行创建新的小部件（例如，文本输入字段、按钮或选择框）始终返回该小部件值的句柄最初，句柄无效，无法访问其值。例如，创建文本输入字段的函数具有以下类型textInputField：：HTMLField（InputField String INVALID）其 中 InputFieldStringINVALID 是 小 部 件 句 柄 的 类 型 虚 类 型INVALID表示句柄尚未验证，从句柄中提取值的函数不能应用于句柄：6value：：InputField a VALID-> aINVALID（以及VALID）是单例类型的另一个实例输入句柄的验证发生在表单提交过程这反映在提交操作的类型中：Submit：：InputHandle h=> h INVALID->（h VALID-> CGI（））-> HTMLField（）函数submit在小部件类型上重载。它将h INVALID类型的无效小部件作为第一个参数，并将h VALID-> CGI（）类型的回调操作作为第二个参数，以生成HTMLField（）。回调操作是通过类型为h VALID的已验证小部件参数化的。小部件类型的这种变化要求重载不能简单地在小部件的类型 上 执 行 ， 而 是 在 类 型 构 造 器 上 执 行 ， 该 类 型 构 造 器 通 过 其VALID/INVALID类型参数抽象小部件类型[6]价值的类型化被简化了。在实现中，value被重载以处理不同类型的句柄，而不仅仅是InputField。T·希曼241不幸的是，这种安排有一个陷阱。假设一个表单包含两个输入小部件，回调动作必须同时处理这两个小部件。在这种情况下，小部件的两个句柄可能都具有类型InputField字符串INVALID虽然将其中一个句柄传递给回调函数很容易，但将两个句柄都传递并不简单。简单地将它们配对会产生类型为（InputField String INVALID，InputField String INVALID）但这种类型不是h INVALID的形式。当然，对于任意的句柄元组和句柄列表，同样的问题也会出现。在这两种情况下，结果类型都没有提交类型所需的形式。事实证明，一些新引入的数据类型拯救了这一天。对于每个要与句柄一起使用的数据构造函数，必须定义一个提升版本例如数据F2 a b x = F2（a x）（b x）定义提升对的数据类型F2，而数据FL a x = FL [a x]定义提升列表的数据类型FL将提升的配对构造函数应用于两个输入句柄会产生类型为F2（InputField String）（InputField String）INVALID它 确 实 具 有 h INVALID 的 形 式 （ 其 中 h 是 F2 （ InputField String ）（InputField String）），因此是提交的第一个合适的参数。要使F2和FL成为可接受的输入句柄，它们需要成为类InputHandle的成员：实例（InputHandle h）=> InputHandle（FL h）其中.instance（InputHandle h1，InputHandle h2）=> InputHandle（F2 h1 h2）其中.最后，但并非最不重要的是，如果我们不想提交任何数据（臭名昭著的继续按钮），数据F0 x = F0显 然 ， F0INVALID 具 有 所 需 的 形 式 hINVALID ， 并 且 可 以 成 为InputHandle的实例：实例InputHandle F0，其中...T·希曼2424.2使用高阶统一的在上一小节中概述的Haskell98解决方案的问题正是使用了虚假的数据构造函数，如F2和FL。很难向非专业的Haskell程序员解释，他们不能简单地构建一个包含句柄的任意数据结构事实上，F2和FL实际上是由类型系统的弱点造成的工件，只使用标准的pair和list类型构造函数会更自然。出于这个原因，我们一直在寻找摆脱这些人工制品的方法返回到一对输入句柄（InputField String INVALID，InputField String INVALID）我们可以看到，这种类型可以通过将其视为高阶统一问题来统一为hINVALID。也就是说，我们不局限于在统一过程中替换构造函数项，而是允许 某 些 lambda 项 。 在 这 个 例 子 中 ， 将 h 映 射 到 \x-> （ InputFieldString x，InputField String x）的替换可以完成这项工作。众所周知，高阶统一化是一个不可判定的问题，而且具有高度的非确定性[3]，因此在类型推理器中引入成熟的高阶统一化是不可取的。特别是，分析表明[13]，可以构造Huet不幸的是，标准程序不能扩展到自动选择可接受的解决方案，因为如果没有进一步的信息，这些信息就不能从统一问题中导出因此，我们将高阶统一化限制为引导高阶统一化[13]，其中lambda项的集合受到限制，并且统一化过程所选择的替换由单独提供的替换集合引导特别地，由Huet的高阶统一过程生成的替换f<$→λx m.c（h1x m）. （hn xm）其中f是自由变量，h1，...，h n是新引入的自由变量，c是常数或约束变量（即，，xm之一）。这些替换是为非刚性类型的方程生成的，其中一侧上的头符号是自由变量f，而另一侧上的头符号另一侧是常数（例如，，c）。在引导的高阶统一中，我们不使用一般的替换，而是依赖于程序员提供的替换。由于我们只对重载时应用它们感兴趣，所以我们将替换的指定绑定到特定类型类的实例声明。例如，在上面的submit函数上下文中考虑的InputHandle类的情况下，我们提供以下实例声明T·希曼243instance（InputHandle h1，InputHandleh2）=> InputHandle（\x->（h1 x，h2 x））本宣言的后果如下：当试图统一（InputHandle h）=>h无效=？=（InputField String INVALID，InputField字符串INVALID）并且我们知道InputHandle h必须保持（在类型检查提交到一对句柄的应用程序时的典型情况），然后类型检查器应用替换\x->（h1 x，h2 x）来获得（InputHandle h1，InputHandle h2）=>(h1INVALID，h2 INVALID）=？=（InputField StringINVALID，InputField字符串INVALID）然后很容易地将其简化（通过一阶统一的）为解h1 =？=InputField字符串h2 =？=InputField字符串满足所有约束条件。4.3用于提交验证的替代API让这一次，我们不清楚回调操作是否必须看到小部件处理程序。相反，提交函数可能会在验证后从处理程序中提取值，并直接将它们传递给回调。(We通过只查看一种类型句柄（Hdl a.）SubmitHandle：：Hdl a->（a-> CGI（））-> HTMLField（）虽然这种类型在只有一个句柄的情况下工作得很好，但句柄对和句柄列表的问题会加剧。让submitVoid：：（）->（（）-> CGI（））-> HTMLField（）submitPair：：（Hdl a，Hdl b）->（（a，b）-> CGI（））->HTMLField（）SubmitList：：[Hdl a]->（[a]-> CGI（））-> HTMLField（）比较这三种类型，看起来回调操作的参数类型应该是句柄类型的函数这个函数SH只是去掉了句柄。结果类型为submitGeneric：：h->（SH h-> CGI（））-> HTMLField（）其中SH必须至少满足以下方程：SH（Hdl a）= aT·希曼244SH（）=（）SH（h1，h2）=（SH h1，SH h2）SH [h1]= [SH h1]更准确地说，我们可以定义SH（H t）=tSH（C）=CSH（f t）=（SHf）（SHt）其中H代表Hdl，C代表常量（任意类型），f和t是构造函数变量。此外，我们将C限制为只能在多项式数据构造函数（不包含函数类型）上运行这种限制不仅简化了开发，而且也是应用程序所需要的关键是验证函数应该在调用它的地方执行它的职责如果数据结构包含处理或返回句柄的函数，那么验证函数最多只能将这些函数强制转换为稍后执行所需检查的函数然而，这种潜在的延迟违背了验证的意图尚待确定SH诱导的转化sh_t：：kr。类型t的值。为了简单起见，我们首先构造一个h-> SH h类型的函数，然后考虑实际的验证函数。幸运的是，SH在类型级别上的递归定义几乎遵循Hinze [9]定义因此，我们只需要定义一个函数unHdl：：Hdl a-> a然后设置shh t：：=unHdl对于其余的情况，则回到一般恒等函数的定义。即sh（）：：=λx.xsh Int：：=λx.x对于其余的基类型，sh（t1，t2）：：λ = λ（x1，x2）. （sht1：：x1，sht2：：x2）sht1+ t2：：λ x= λx. Inlx1的casex→Inl（sht1：：x1）Inlx2→Inl（sht2：：Hdlx2）实际上，除了unHdl之外，还有一个函数validate，它的类型是validate：：Hdl a-> Either [String] a也就是说，它要么返回值本身，要么返回采用字符串列表形式的错误消息。显然，Either [String]是一个monad，因此我们从错误处理机制的细节中抽象出来，假设T·希曼245它可以用单子来表达因此，仍然需要定义一个函数processHdl，它传播类型为process：：Monad m => Hdl a-> m a通过一个可能包含HDLs的值以下是ph的一般定义（进程句柄）：ph：：m. Monadmh→m（SHh）phH t：：=processph（）：：=return phInt：：=return对于其余的基类型，ph =（t1，t2）：：λ = λ（x1，x2）. do y1← pht1：：x1y2←pht2：：x2return（y1，y2）ph =t1+ t2：：λx。Inlx1的casex→doy1←pht1：：x1return（Inly1）Inlx2→doy2←pht2：：x2return（Inry2）Hinze方法的美妙之处不幸的是，正如理论[9]所提出的那样，它不允许在基本情况下使用重载，这是使我们的定义工作所必需的。或者，一个仅限于一阶类型的版本可以很容易地使用函数逻辑重载来实现[4]。然而，这个任务可能会更加乏味，因为我们必须为每一个将被包装在句柄上的数据类型手动专门化求和和乘积类型的情况4.4限制Widget句柄输入提交原语的投资回报是什么当然，我们获得了很多编程上的便利：输入小部件不需要给出明确的名称，由于小部件名称而导致的不一致问题消失了，浏览器和脚本之间的通信是键入的，并且由于输入字段中的无效条目而导致的所有错误都被系统捕获，而然而，一个紧迫的问题仍然存在。它是由小部件句柄的词法作用域和句柄的实际生存期之间的不匹配引起的句柄T·希曼246问（...name F-textInputField（fieldSIZE 40）...submit F0（getMoreInput nameF）empty）getMoreInput name FF0 =ask（...提交名称（操作为空）Fig. 1. 错误的WASH/CGI脚本它在与该Web页面关联的任何回调操作开始构造响应页面之前结束它对应于一个交互周期：将表单交付给浏览器，并处理答案以构建下一个表单。这些检查点可以很容易地在程序中通过查找组合子ask来确定，它启动了一个新表单的创建因此，实际生存期也对应于程序文本的一部分为了理解实际生存期的重要性，我们需要一些关于小部件实现的信息。对于表单中的任何输入字段，它的窗口小部件构造函数至少在两种不同的模式下执行多次。最初，构造函数构建小部件的内部表示，即HTML元素。当表单与此同时，它构建了错误页面的一部分，仅在提交无法验证的情况下使用。接下来，一个提交函数被激活，它试图验证传递给它的句柄。如果这个过程成功，它将控制传递给它的回调动作。但是，如果其中一个句柄无法验证，它会将包含最后一个表单的错误页发送回浏览器，以便用户可以重新输入数据。为方便起见，在此表单中，未验证的小部件将以可视方式标记，其他小部件将初始化为先前输入的值现在，问题如下。假设一个动作在一个自由变量中保留了一个无效的句柄，并在随后的交互动作中将其传递给提交函数 如果条目现在有效，那么就没有问题，程序将按预期继续运行。否则，submit将重新显示最后一个表单。但是，此表单不是错误输入的表单，因此无法更正错误（除非使用后退按钮和一些猜测）。图1给出了这种行为的一个示例。第一个Web页面（前五行）有一个文本输入字段，它与句柄名F相关联。该页面包含一个提交按钮，该按钮不验证任何内容（指示T·希曼247F0）。但是，回调操作getMoreInputnameF包含对（无效）句柄nameF的引用。getMoreInput操作生成一个新的Web页面，并通过该页面上的按钮提交nameF字段。在极端情况下，第二个页面没有输入字段，只是显示一些文本（例如，条款和条件）和一个在第一页输入无效名称的用户只有在点击第二页上的当然，这是一个令人困惑的情况。好消息是，我们也可以用类型系统来解决这个编程错误我们的解决方案依赖于秩2类型的使用它的灵感来自于Launchbury和Peyton Jones技巧是用一个幻影类型变量索引底层的CGImonad这个幻影类型变量也出现在输入句柄的类型中（作为一个额外的类型参数）输入小部件的创建具有以下修改的类型textInputField：：HTMLField x（InputField String x INVALID）哪里type HTMLField x a = WithHTML（CGI x）（）-> WithHTML（CGI x）a因此，提交函数Submit：：InputHandle h=> h x无效->（h x VALID-> for all y.CGI y（））-> HTMLField x（）实际上，h x VALID中的x参数并不重要，因为值函数在此参数中是多态的value：：InputField a x VALID-> aF0、F2和FL也需要修改，以接受另一个类型参数，它们只是传递给它们的参数：数据F0 x y = F0数据F2 a b x y = F2（a x y）（b xy）数据FL a x y = FL [a x y]这种方法有效地排除了范围不匹配错误。例如，在图中的程序中，函数调用submit F0（getMoreInput nameF）为空%1不进行类型检查。当然，结束 部 分 是 在 要 提 交 的 回 调 参 数 中 使 用 nameF 。 下 面 是 从 nameF ： ：InputField String x INVALID的假设开始发生的情况：• Submit name F accept emptyhas type WithHTML（CGI x）（）• F0用于类型 F0 x INVALIDT·希曼248• getMoreInputnameF的类型为所有yz。F0 y z-> CGI x（）（注意，x不能被普遍量化，因为表达式中出现了nameF，因此对nameF的假设以及类型变量 x必须出现在环境中）• 但getMoreInputnameF必须假定所有y的类型。F0 y VALID-> CGI y（）• 由于期望的类型不是第一个类型的泛型实例，类型推断在这一点上失败。报告的错误是类型变量x不能泛化。最后，事实证明，在某些情况下，这种类型的限制性太强。例如，考虑一个具有几个不同输入字段的Web页面，其中一组按钮（或选择框）决定考虑哪些其他输入字段。也就是说，必须验证的小部件句柄取决于一个或多个输入字段的值或者他们甚至可以随机选择。当前编程模型的明显扩展要求我们首先验证并提交选择器字段，然后以某种方式验证特定选择所需的字段集这可以通过使用以下类型的提交函数来完成Submitx：：InputHandle h=> h x无效->（h x VALID->（对于所有h输入句柄h=> h-> Either [String]（h->（对于所有y。[String]（CGI y（）-> HTMLField x（）这个想法是参数函数接受一个经过验证的输入句柄，并使用它的值来选择更多的输入句柄进行验证。第二个参数是验证函数。它的类型在要处理的输入句柄的种类和类型上是多态的，但是在同一类型上专用于在用x索引的线程中创建的句柄。由于验证可能失败，函数不会直接返回action，而是再次将其包装到错误monadEither [String]5相关工作Thiemann [16]使用具有函数依赖的多参数类型类来生成正确的HTML。我们已经简化了基本方法，即使用两个参数类型类AddTo将元素与其父元素关联到 纯 Haskell98 方 法 ， 该 方 法 依 赖 于 许 多 专 用 的 单 参 数 类 型 类（AdmitChild... ）.我们重新表达了多参数T·希曼249使用函数逻辑重载实现转换函数的类[4]。WASH/CGI [17]为探索提交功能提供了动力。本文通过引入一些提交类型来扩展这项工作，这些类型保证浏览器发布的数据与服务器端脚本期望的数据之间没有不匹配在技术方面，Sulzmann和其他人[5]已经引入了一个采用约束处理规则的可编程类型系统该系统也可以表达函数逻辑重载支持的大多数功能，但它依赖于约束逻辑编程作为其基础。泛型编程的工作（例如，Hinze我们已经证明，对Hinze框架的一个相当小的扩展事实上，由于他的框架中的函数可以与Haskell 98 [10]顺利集成，因此我们不认为所需的扩展是一个根本问题。6结论DSL的WASH家族的发展导致了许多有趣的打字问题。 我们已经为这些类型问题开发了解决方案，有时将它们编码到Haskell 98中，但也依赖于语言的扩展，如函数逻辑重载，匿名类型函数，秩2多态性和Hinze的泛型编程框架。所提出的解决方案保证了WASH脚本的高级属性：生成的HTML文档的正确性以及浏览器提交的数据与Web浏览器预期的数据之间的一致性。确认感谢Matthias Neubauer仔细阅读了本文的草稿引用[1] A. 诉阿霍河Sethi和J.D. 厄尔曼制造原则、技术和工具。Addison-Wesley，1986年。[2] J. A. Brzozowski.正则表达式的导数。Journal of the ACM，11（4）：481[3] G. 多维克 高阶统一和匹配。 以. Robinson和A. Voronkov，编者，《自动推理手册》，第2卷，第16章，第1009-1062页北荷兰，2001年。T·希曼250[4] M. Gasbichler，M.Neubauer，M.Sperber，和P.蒂曼功能逻辑过载。在J.Mitchell ， 编 辑 ， Proc.29th Annual ACM Symposium onPrinciples ofProgramming Languages，第233-244Press.[5] K. Glynn，P. Stuckey，and M.苏兹曼类型类和约束处理规则。第一次基于规则的约束推理和编程研讨会，2000年7月。[6] M. 哈 纳 斯 功 能 集 成 到 逻 辑 编 程 ： 从 理 论 到 实 践 。 Journal of LogicProgramming，19（20）：583[7] M. 哈纳斯一种用于函数和逻辑编程的统一计算模型在N. D. Jones，编辑，Proc.24th Annual ACM Symposium on Principles of ProgrammingLanguages，第80-93页，巴黎，法国，1997年1月。Press.[8] Haskell 98是一种非严格的纯函数式语言。http://www.haskell。org/definition，Dec. 1998年[9] R.欣兹多型值具有多型类型。Science of Computer Programming，43（2[10] R. Hinze和S.佩顿·琼斯。可派生类型类。In G. Hutton，编辑，2000年ACMSIGPLAN Haskell研讨会论文集，第41卷，理论计算机科学电子笔记，加拿大蒙特利尔，9月。2001. Elsevier Science.[11] M. P.琼斯。具有函数依赖关系的类型类。In G. Smolka，编辑，Proc. 第9届欧洲编程研讨会，编号1782，计算机科学讲义，第230-244页，柏林，德国，2000年3月。施普林格出版社。[12] Launchbury和S. L.佩顿·琼斯。在Haskell。Lisp and Symbolic Comput