• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Programming languages and systems >Extending Hindley-Milner Type Inference with Coercive Structural Subtyping
【24h】

Extending Hindley-Milner Type Inference with Coercive Structural Subtyping

机译：用强制结构子类型扩展Hindley-Milner类型推断

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

摘要

We investigate how to add coercive structural subtyping to a type system for simply-typed lambda calculus with Hindley-Milner polymorphism. Coercions allow to convert between different types, and their automatic insertion can greatly increase readability of terms. We present a type inference algorithm that, given a term without type information, computes a type assignment and determines at which positions in the term coercions have to be inserted to make it type-correct according to the standard Hindley-Milner system (without any subtypes). The algorithm is sound and, if the subtype relation on base types is a disjoint union of lattices, also complete. The algorithm has been implemented in the proof assistant Isabelle.
机译：我们研究如何为具有Hindley-Milner多态性的简单类型lambda演算的类型系统添加强制结构子类型。强制允许在不同类型之间进行转换，并且它们的自动插入可以大大提高术语的可读性。我们提供一种类型推断算法，给定没有类型信息的术语，该算法可以计算类型分配，并根据标准的Hindley-Milner系统（不包含任何子类型）确定必须在术语强制中插入哪些位置以使其类型正确）。该算法是合理的，并且如果基本类型的子类型关系是晶格的不交集并集，那么该算法也很完善。该算法已在证明助手Isabelle中实现。

著录项

  • 来源
    《Programming languages and systems》|2011年|p.89-104|共16页
  • 会议地点 Kenting(CT);Kenting(CT)
  • 作者

    Dmitriy Traytel; Stefan Berghofer; Tobias Nipkow;

  • 作者单位

    Technische Universitaet Muenchen Institut fuer Informatik, Boltzmannstrasse 3, 85748 Garching, Germany;

    Technische Universitaet Muenchen Institut fuer Informatik, Boltzmannstrasse 3, 85748 Garching, Germany;

    Technische Universitaet Muenchen Institut fuer Informatik, Boltzmannstrasse 3, 85748 Garching, Germany;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 程序设计、软件工程;
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号