Metraipolis › archive › dc_09bddd89cecd

Modular Composition of Inductive Types Using Lean Meta-programming — arXiv:2609.25427

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.25427
License (as archived): CC0-1.0
Archived: 2026-10-08T15:16:14.680Z
SHA-256 of the archived text: 8fac09971940be221b9043aca60c54fe63db47324f34da281efec00737e36b9a
Stable URL of this page: https://metraipolis.com/documento/dc_09bddd89cecd

How to cite

Modular Composition of Inductive Types Using Lean Meta-programming — arXiv:2609.25427 — arXiv (en), https://arxiv.org/abs/2609.25427 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_09bddd89cecd (Metraipolis archive dc_09bddd89cecd, sha256 8fac09971940be221b9043aca60c54fe63db47324f34da281efec00737e36b9a)

BibTeX

@misc{dc09bddd89cecd,
  title = {Modular Composition of Inductive Types Using Lean Meta-programming — arXiv:2609.25427},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.25427},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_09bddd89cecd; sha256 8fac09971940be221b9043aca60c54fe63db47324f34da281efec00737e36b9a},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.25427. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: calcolo e infrastrutture (retro-catalogo arXiv: annunci del 2026-09-23 in cs.SE).
Categorie arXiv: Programming Languages (cs.PL) ; Logic in Computer Science (cs.LO); Software Engineering (cs.SE).
Pagina del lavoro: https://arxiv.org/abs/2609.25427 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-08T14:42:48.188Z dalla pagina https://arxiv.org/catchup/cs.SE/2026-09-23?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).