首页> 外文期刊>Science of Computer Programming >Deriving a complete type inference for Hindley-Milner and vector sizes using expansion
【24h】

Deriving a complete type inference for Hindley-Milner and vector sizes using expansion

机译:使用扩展推导Hindley-Milner和向量大小的完整类型推断

获取原文
获取原文并翻译 | 示例

摘要

Type inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract interpretation. We observe that completeness results in the abstract interpretation literature can be used to derive type inferences that are backward complete, implying that type annotations cannot improve the result of type inference, thus making type annotations optional. The resulting algorithm is similar to that of Milner-Mycroft, that is, it infers Hindley-Milner types while allowing for polymorphic recursion. Although undecidable, we present a practical check that reliably distinguishes typeable from untypeable programs. Instead of type schemes, we use expansion to instantiate types. Since our expansion operator is agnostic to the abstract domain, we are able to apply it not only to types. We illustrate this by inferring the size of vector types using systems of linear equalities and present practical uses of polymorphic recursion using vector types.
机译:类型推断和程序分析都可以推断程序的静态属性。但是,它们是使用非常不同的技术构造的。我们通过使用抽象解释从指称语义中推导类型推断来调和这两种方法。我们观察到抽象解释文献中的完整性结果可用于推导向后完成的类型推断,这意味着类型注释不能改善类型推断的结果,从而使类型注释成为可选的。生成的算法与Milner-Mycroft的算法相似,也就是说,它可以推断Hindley-Milner类型,同时允许多态递归。尽管无法确定,但我们提出了一种实用的检查方法,可以可靠地区分可键入程序与不可键入程序。代替类型方案,我们使用扩展实例化类型。由于扩展运算符与抽象域无关,因此我们不仅可以将其应用于类型。我们通过使用线性等价系统推断向量类型的大小来说明这一点,并介绍了使用向量类型进行多态递归的实际应用。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号