使用Lean元编程的归纳类型模块化组合
Modular Composition of Inductive Types Using Lean Meta-programming
浏览论文内容
中文总结 AI 辅助
本文提出基于元编程的归纳类型与函数实现组合算法及Lean语法扩展，实现模块化重用与扩展，并通过三子语言组合案例验证其特性与局限。
中文摘要 AI 辅助
归纳类型是许多编程语言和定理证明语言中无处不在的构建块。归纳类型是一组封闭的构造子，通过这些构造子可以创建该类型的值。然而，一旦类型被定义，该集合就不能再扩展。这限制了在定义类型及其值上操作的函数时的可扩展性、重用性和关注点的模块化分离。这种限制体现在表达式问题中，即在几乎所有编程语言中，在不修改或重新编译现有构造子的情况下，向表达式语言添加新的语法构造子是一个挑战。本文提出了基于元编程的归纳类型和函数实现组合算法。此外，还提出了一组实现这些算法的Lean证明助手的语法扩展。该框架允许对Lean类型和函数定义的子集进行模块化重用、组合和扩展。此外，在类型理论和实现层面讨论了组件类型与组合类型之间的语义子类型关系。该框架通过一个案例研究进行了演示，该案例研究涉及将三个子语言的语法和语义构件组合成一种语言。该案例研究突出了组合框架的特点和局限性。
英文摘要
Inductive types are ubiquitous building blocks in many programming and theorem proving languages. An inductive type is a closed set of constructors from which values of the type can be created. That set cannot be extended though once a type is defined. This limits extensibility, reuse, and modular separation of concerns when defining types and functions operating over their values. This limitation is manifested in the expression problem, where extending an expression language with new syntactic constructors without having to modify or re-compile existing ones is a challenge in almost all programming languages. This paper presents inductive type and function implementation composition algorithms based on meta-programming. In addition, a set of syntactic extensions to the Lean proof assistant implementing those algorithms are presented. This framework allows for modular reuse, composition, and extension of a subset of Lean type and function definitions. In addition, semantic subtyping relations between component and composite types are discussed both at the type theoretic and implementation levels. The framework is demonstrated on a case study, involving the composition of syntactic and semantic artifacts of three sublanguages into one language. The case study highlights both the features and limitations of the composition framework.
发表机构
- Qualgebra
机构由 AI 辅助整理，请以论文原文为准。
