Well-Typed Programs Can't Be Blamed
Well-Typed Programs Can't Be Blamed
复制标题
不能责怪类型良好的程序
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
R. Findler
中科院分区：
文献类型：
--
作者：
P. Wadler;R. Findler
我们引入了指责演算，它将芬德勒和费莱森合同中的指责概念添加到一个类似于Siek和Taha的渐进型以及弗拉纳根的混合型的系统中。我们通过将通常的子类型的概念分解为积极的和消极的子类型来描述可能出现积极和消极指责的地方，并表明这些重新组合产生了天真的子类型。朴素的子类型以前出现在不健全的类型系统中，但我们相信这是第一次在建立类型健全的过程中发挥作用。
We introduce the blame calculus , which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types . We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtypes, and show that these recombine to yield naive subtypes. Naive subtypes previously appeared in type systems that are unsound, but we believe this is the first time naive subtypes play a role in establishing type soundness.