关于非自由具体数据类型构造函数的实现
计算机科学中的逻辑
2016-08-14 v1 编程语言
摘要
许多算法使用带有某些附加不变量的具体数据类型。满足不变量的值集通常是某些等式理论的等价类的代表元集。例如，有序列表就是关于交换性的一个特定代表元。结合律、中性元、幂等性等理论也非常常见。现在，当人们想要组合各种不变量时，可能很难找到合适的代表元并有效地实现不变量。在整个程序中保持不变量更加困难且容易出错。通常，程序员使用两种技术的组合来解决这个问题：为代表元定义适当的构造函数，以及通过编译器验证确保这些函数的一致使用。确保一致性的常用方法是使用代表元的抽象数据类型；不幸的是，代表元上的模式匹配丢失了。一种更具吸引力的替代方案是定义带有私有构造函数的具体数据类型，以便同时保证编译器验证和代表元上的模式匹配。在本文中，我们详细介绍了私有数据类型的概念并研究了构造函数的存在性。我们还描述了一个名为 Moca 的原型，它解决了整个问题……
引用
@article{arxiv.cs/0701031,
title = {On the implementation of construction functions for non-free concrete data types},
author = {Frédéric Blanqui and Thérèse Hardin and Pierre Weis},
journal= {arXiv preprint arXiv:cs/0701031},
year = {2016}
}