In their 1991 paper "Algebraic Reconstruction of Types and Effects," Pierre Jouvelot and David Gifford presented a type-and-effect reconstruction algorithm based on an algebraic structure of effects. Their work is considered a milestone in the development of type-and-effect systems, and has inspired numerous subsequent works in the area of static analysis. However, unlike the later research it spawned, the original algorithm considered a language with higher-rank polymorphism, a feature which is challenging to implement correctly. In this note, we identify subtle bugs related to variable binding in their approach to this feature. We revisit their type system and reconstruction algorithm, and describe the discovered issues.


翻译:在1991年的论文《类型与效应的代数重构》中,Pierre Jouvelot与David Gifford提出了一种基于效应代数结构的类型与效应重构算法。该工作被视为类型与效应系统发展史上的里程碑,对静态分析领域的后续研究产生了深远影响。然而,与受其启发的后续研究不同,原始算法所处理的语言包含高阶多态性——这一特性在正确实现上存在显著挑战。本文指出该算法在处理此特性时涉及变量绑定的若干微妙缺陷。我们重新审视其类型系统与重构算法,并对所发现的问题进行详细阐述。

0
下载
关闭预览

相关内容

在数学和计算机科学之中,算法(Algorithm)为一个计算的具体步骤,常用于计算、数据处理和自动推理。精确而言,算法是一个表示为有限长列表的有效方法。算法应包含清晰定义的指令用于计算函数。 来自维基百科: 算法
【AAAI2021】对比聚类,Contrastive Clustering
专知
26+阅读 · 2021年1月30日
类脑计算的前沿论文,看我们推荐的这7篇
人工智能前沿讲习班
21+阅读 · 2019年1月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
6+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 1月31日
VIP会员
相关VIP内容
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
6+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员