• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Programming languages and systems >Polymorphic Multi-stage Language with Control Effects
【24h】

Polymorphic Multi-stage Language with Control Effects

机译：具有控制效果的多态多阶段语言

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Multi-stage programming (MSP) is a means for run-time code generation, and has been found promising in various fields including numerical computation and domain specific languages. An important problem in designing MSP languages is the dilemma of safety and expressivity; many foundational calculi have been proposed and proven to be type safe, yet, they are not expressive enough. Taha's MetaOCaml provides us a very expressive tool for MSP, yet, the corresponding theory covers its purely functional subset only. In this paper, we propose a polymorphic multi-stage calculus with delimited-control operators. Kameyama, Kiselyov, and Shan proposed a multi-stage calculus with computation effects, but their calculus lacks polymorphism. In the presence of control effects, polymorphism in types is indispensable as all pure functions are polymorphic over answer types, and in MSP languages, polymorphism in stages is indispensable to write custom generators as library functions. We show that the proposed calculus satisfies type soundness and type inference. The former is the key to guarantee the absence of scope extrusion - open codes are never generated or executed. The latter is important in the ML-like programming languages. Following Calcagno, Moggi and Taha's work, we propose a Hindley-Milner style type inference algorithm to obtain principal types for given expressions (if they exist).
机译：多阶段编程（MSP）是一种用于生成运行时代码的方法，并且在包括数值计算和领域特定语言在内的各个领域中都发现了前途。设计MSP语言时的一个重要问题是安全性和表达能力的困境。已经提出了许多基础结石，并证明它们是类型安全的，但它们的表达能力不足。 Taha的MetaOCaml为我们提供了一个针对MSP的非常有表现力的工具，但是，相应的理论仅涵盖了其纯功能子集。在本文中，我们提出了带有定界控制算子的多态多级演算。 Kameyama，Kiselyov和Shan提出了具有计算效果的多阶段微积分，但它们的微积分缺乏多态性。在存在控制效果的情况下，类型中的多态性是必不可少的，因为所有纯函数都比答案类型具有多态性，而在MSP语言中，分阶段的多态性对于将自定义生成器编写为库函数是必不可少的。我们表明，提出的演算满足类型健全性和类型推断。前者是确保不扩大范围的关键-永远不会生成或执行开放代码。后者在类似ML的编程语言中很重要。继Calcagno，Moggi和Taha的工作之后，我们提出了Hindley-Milner样式类型推断算法，以获取给定表达式（如果存在）的主体类型。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号