具有幻影类型和递归模式的实用数据类型专门化
Practical Datatype Specializations with Phantom Types and Recursion Schemes
摘要：
数据类型专门化是子类型化的一种形式，它捕获数据结构上的程序不变量，这些数据结构使用方便直观的数据类型表示法来表示。特别感兴趣的是结构不变量，如良构性。我们研究使用幻影类型来描述数据类型专门化。我们证明了在标准ML的类型系统中可以表达静态检查的专门化。我们还表明，这可以做到这一点的方式，不失去有用的编程设施，如模式匹配的情况下表达式。
英文摘要：
Datatype specialization is a form of subtyping that captures program invariants on data structures that are expressed using the convenient and intuitive datatype notation. Of particular interest are structural invariants such as well-formedness. We investigate the use of phantom types for describing datatype specializations. We show that it is possible to express statically-checked specializations within the type system of Standard ML. We also show that this can be done in a way that does not lose useful programming facilities such as pattern matching in case expressions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
