不确定性之和：细化逐步化

静态类型函数式语言的一个长期缺陷是类型检查无法排除模式匹配失败（运行时匹配异常）。细化类型区分数据类型的不同值；如果用细化标注的程序通过了类型检查，模式匹配失败就变得不可能。不幸的是，细化是类型的整体属性，这加剧了将细化类型添加到非平凡程序的难度。逐步类型探索了如何在静态类型和动态类型之间逐步过渡。我们开发了一种结合细化与不精确性的逐步和类型系统。然后，我们开发了该类型系统的双向版本，排除了过度不精确性，并给出了向具有显式类型转换的目标语言进行类型导向翻译。我们证明了静态子语言不可能有匹配失败，一个类型良好的程序在其类型标注变得不精确时仍保持类型良好，并且使标注变得不精确会导致目标程序在后续失败。这些结果中的若干对应于Siek等人(2015)给出的逐步类型标准。