Collaborative Research: Modular Metaprogramming

软件开发人员依靠高质量的软件库来降低构建复杂应用程序的成本。然而，许多软件库提供了复杂的接口，使库能够适应特定于应用程序的需求。这种复杂性增加了采用的成本，减少了软件重用的好处。研究人员发现，如果底层编程语言为库作者提供了用于在应用程序编译期间推理程序元数据和基于此信息定制库实现的构造，则库可以变得更通用、更易于使用。当前的编程语言以一种不成熟的形式提供了这些特性，编程语言理论的最新状态还没有达到这些特性的组合。研究人员正在推进这一理论，将类型安全和模块化引入这一背景，他们正在与c++标准委员会密切合作，将他们的研究成果转化为工业实践。推理元数据和定制库所需的语言特性组合称为反射元编程。该领域以前的研究为元编程提供了类型安全性和模块化，但没有提供反射性元编程。研究者们正在研究反射元编程的类型安全性，方法是仔细地集成：1)提供对值和类型的计算并对所有程序元数据提供反射的元语言，2)分类类型的工具，以及3)使用依赖类型提供与元语言挂钩的类型系统。通过开发一个更可靠和更具表现力的元编程系统，本研究提高了软件库开发人员和用户的编程效率，因为模块化类型系统将在开发周期的早期发现更多的错误。

Software developers rely on high-quality software libraries to mitigate the cost of building complex applications. However, many software libraries provide complex interfaces to make the library adaptable to application-specific needs. This complexity raises the cost of adoption and reduces the benefits of software reuse. Researchers discovered that libraries can be made more versatile and easier to use if the underlying programming language provides library authors with constructs for reasoning, during the compilation of the application, about program metadata and for customizing the library implementation based on this information. Current programming languages provide these features in an immature form and the state of the art in programming language theory does not yet reach this combination of features. The investigators are advancing the theory to bring type safety and modularity to this context and they are working closely with the C++ Standards Committee to transfer their results to industrial practice.The combination of language features needed to reason about metadata and customize libraries is called reflective metaprogramming. Previous research in this area provides type safety and modularity for metaprogramming but not reflective metaprogramming. The investigators are researching type safety for reflective metaprogramming through a careful integration of 1) a meta-language that provides computation over values and types and that provides reflection over all the program's metadata, 2) a facility for classifying types, and 3) a type system that provides hooks into the meta-language using dependent types. By developing a more reliable and expressive metaprogramming system, this research improves programmer productivity for both the developers and users of software libraries because many more bugs will be caught early in the development cycle by the modular type system.