TyDe '25: "The Conatural Numbers Form ..."
The Conatural Numbers Form an Exponential Commutative Semiring
Szumi Xie and Viktor Bense
(Eötvös Loránd University, Hungary)
Conatural numbers are a coinductive type dual to the inductively defined natural numbers. The conatural numbers can represent all natural numbers and an extra element for infinity, this can be useful for representing the amount of steps taken by a possibly non-terminating program. We can define functions on conatural numbers by corecursion, however proof assistants such as Agda require the corecursive definitions to be guarded to make sure that they are productive. This requirement is often too restrictive, as it disallows the corecursive occurrence to appear under previously defined operations. In this paper, we explore some methods to solving this issue using the running examples of multiplication and the commutativity of addition on conatural numbers, then we give comparisons between these methods. As the main result, this is the first proof that conatural numbers form an exponential commutative semiring in cubical type theory without major extensions.
@InProceedings{TyDe25p52,
author = {Szumi Xie and Viktor Bense},
title = {The Conatural Numbers Form an Exponential Commutative Semiring},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {52-63},
doi = {10.1145/3759538.3759654},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "A Formalization of Opaque ..."
A Formalization of Opaque Definitions for a Dependent Type Theory
Nils Anders Danielsson and Eve Geng
(University of Gothenburg and Chalmers University of Technology, Sweden; Chalmers University of Technology, Sweden)
Definitions allow for reuse of code. Typical type-checkers for dependently typed programming languages automatically unfold definitions, but excessive unfolding can lead to types that are hard to read, or performance issues. Such problems can be mitigated through the use of opaque definitions, which give the programmer control over when unfolding is allowed. However, subject reduction fails to hold for certain designs.
We study the metatheory of a type theory with opaque definitions, inspired by Agda. We give typing and reduction rules and show that the type theory enjoys properties like subject reduction, normalization, consistency, and decidability of conversion. The development is fully mechanized in Agda.
@InProceedings{TyDe25p39,
author = {Nils Anders Danielsson and Eve Geng},
title = {A Formalization of Opaque Definitions for a Dependent Type Theory},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {39-51},
doi = {10.1145/3759538.3759653},
year = {2025},
}
Publisher's Version
TyDe '25: "A Formalization of Opaque ..."
A Formalization of Opaque Definitions for a Dependent Type Theory
Nils Anders Danielsson and Eve Geng
(University of Gothenburg and Chalmers University of Technology, Sweden; Chalmers University of Technology, Sweden)
Definitions allow for reuse of code. Typical type-checkers for dependently typed programming languages automatically unfold definitions, but excessive unfolding can lead to types that are hard to read, or performance issues. Such problems can be mitigated through the use of opaque definitions, which give the programmer control over when unfolding is allowed. However, subject reduction fails to hold for certain designs.
We study the metatheory of a type theory with opaque definitions, inspired by Agda. We give typing and reduction rules and show that the type theory enjoys properties like subject reduction, normalization, consistency, and decidability of conversion. The development is fully mechanized in Agda.
@InProceedings{TyDe25p39,
author = {Nils Anders Danielsson and Eve Geng},
title = {A Formalization of Opaque Definitions for a Dependent Type Theory},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {39-51},
doi = {10.1145/3759538.3759653},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "Unification Modulo Isomorphisms ..."
Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search
Satoshi Takimoto, Sosuke Moriguchi, and Takuo Watanabe
(Institute of Science Tokyo, Japan)
Type-based library search allows developers to efficiently find reusable software components by their type signatures, as exemplified by tools like Hoogle. This capability is especially important in interactive theorem provers (ITPs), where reusing existing proofs can greatly accelerate development. Previous type-based library search tools for ITPs, such as SearchIsos and Loogle, support only a subset of desirable search flexibilities, including argument reordering, currying/uncurrying, generalisation, and the inclusion of extra premises. However, none can handle all these flexibilities simultaneously, resulting in missed relevant matches. In this work, we propose a type-based library search method based on equational unification modulo a set of type isomorphisms for dependent product/sum types, enabling all the desired search flexibilities. We present a semi-algorithm for this equational unification and provide a prototype implementation to demonstrate the feasibility of our approach.
@InProceedings{TyDe25p15,
author = {Satoshi Takimoto and Sosuke Moriguchi and Takuo Watanabe},
title = {Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {15-25},
doi = {10.1145/3759538.3759651},
year = {2025},
}
Publisher's Version
TyDe '25: "Representing Data Structures ..."
Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL
Nicolas Rodriguez, Alberto Pardo, and Marcos Viera
(Universidad de la República, Uruguay)
Invariants are an essential aspect to take into account for the correct implementation of data structures and their operations. This paper explores how to encode and enforce invariants at type level in Haskell, using Binary Search Trees (BSTs) and AVL trees as case studies. This means the encoding of invariants at type level using advanced features of Haskell type system and their later verification by the type checker. We compare three approaches for the type-level encoding of invariants: fully externalist, externalist, and internalist, each offering a different balance between modularity, safety, and complexity. We also show how to systematically extract standard implementations from correct, invariant-based code.
@InProceedings{TyDe25p26,
author = {Nicolas Rodriguez and Alberto Pardo and Marcos Viera},
title = {Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {26-38},
doi = {10.1145/3759538.3759652},
year = {2025},
}
Publisher's Version
TyDe '25: "Representing Data Structures ..."
Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL
Nicolas Rodriguez, Alberto Pardo, and Marcos Viera
(Universidad de la República, Uruguay)
Invariants are an essential aspect to take into account for the correct implementation of data structures and their operations. This paper explores how to encode and enforce invariants at type level in Haskell, using Binary Search Trees (BSTs) and AVL trees as case studies. This means the encoding of invariants at type level using advanced features of Haskell type system and their later verification by the type checker. We compare three approaches for the type-level encoding of invariants: fully externalist, externalist, and internalist, each offering a different balance between modularity, safety, and complexity. We also show how to systematically extract standard implementations from correct, invariant-based code.
@InProceedings{TyDe25p26,
author = {Nicolas Rodriguez and Alberto Pardo and Marcos Viera},
title = {Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {26-38},
doi = {10.1145/3759538.3759652},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "Unification Modulo Isomorphisms ..."
Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search
Satoshi Takimoto, Sosuke Moriguchi, and Takuo Watanabe
(Institute of Science Tokyo, Japan)
Type-based library search allows developers to efficiently find reusable software components by their type signatures, as exemplified by tools like Hoogle. This capability is especially important in interactive theorem provers (ITPs), where reusing existing proofs can greatly accelerate development. Previous type-based library search tools for ITPs, such as SearchIsos and Loogle, support only a subset of desirable search flexibilities, including argument reordering, currying/uncurrying, generalisation, and the inclusion of extra premises. However, none can handle all these flexibilities simultaneously, resulting in missed relevant matches. In this work, we propose a type-based library search method based on equational unification modulo a set of type isomorphisms for dependent product/sum types, enabling all the desired search flexibilities. We present a semi-algorithm for this equational unification and provide a prototype implementation to demonstrate the feasibility of our approach.
@InProceedings{TyDe25p15,
author = {Satoshi Takimoto and Sosuke Moriguchi and Takuo Watanabe},
title = {Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {15-25},
doi = {10.1145/3759538.3759651},
year = {2025},
}
Publisher's Version
TyDe '25: "Gradual Metaprogramming ..."
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, and Rocky Liu
(Indiana University, USA; Meta, USA)
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenges in debugging the generation of data pipelines: an error in a Python DSL script is often detected too late, after the execution of the script, and the source code location that triggers the error is hard to pinpoint.
In this paper, we focus on the scenario where a DSL embedded in Python (so it is dynamically-typed) generates data pipeline description code that is statically-typed. We propose gradual metaprogramming to (1) provide a migration path toward statically typed DSLs, (2) immediately provide earlier detection of code generation type errors, and (3) report the source code location responsible for the type error. Gradual metaprogramming accomplishes this by type checking code fragments and incrementally performing runtime checks as they are spliced together. We define MetaGTLC, a metaprogramming calculus in which a gradually-typed metalanguage manipulates a statically-typed object language, and give semantics to it by translation to the cast calculus MetaCC. We prove that successful metaevaluation always generates a well-typed object program and mechanize the proof in Agda.
@InProceedings{TyDe25p1,
author = {Tianyu Chen and Darshal Shetty and Jeremy G. Siek and Chao-Hong Chen and Weixi Ma and Arnaud Venet and Rocky Liu},
title = {Gradual Metaprogramming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1-14},
doi = {10.1145/3759538.3759650},
year = {2025},
}
Publisher's Version
TyDe '25: "Representing Data Structures ..."
Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL
Nicolas Rodriguez, Alberto Pardo, and Marcos Viera
(Universidad de la República, Uruguay)
Invariants are an essential aspect to take into account for the correct implementation of data structures and their operations. This paper explores how to encode and enforce invariants at type level in Haskell, using Binary Search Trees (BSTs) and AVL trees as case studies. This means the encoding of invariants at type level using advanced features of Haskell type system and their later verification by the type checker. We compare three approaches for the type-level encoding of invariants: fully externalist, externalist, and internalist, each offering a different balance between modularity, safety, and complexity. We also show how to systematically extract standard implementations from correct, invariant-based code.
@InProceedings{TyDe25p26,
author = {Nicolas Rodriguez and Alberto Pardo and Marcos Viera},
title = {Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {26-38},
doi = {10.1145/3759538.3759652},
year = {2025},
}
Publisher's Version
TyDe '25: "Unification Modulo Isomorphisms ..."
Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search
Satoshi Takimoto, Sosuke Moriguchi, and Takuo Watanabe
(Institute of Science Tokyo, Japan)
Type-based library search allows developers to efficiently find reusable software components by their type signatures, as exemplified by tools like Hoogle. This capability is especially important in interactive theorem provers (ITPs), where reusing existing proofs can greatly accelerate development. Previous type-based library search tools for ITPs, such as SearchIsos and Loogle, support only a subset of desirable search flexibilities, including argument reordering, currying/uncurrying, generalisation, and the inclusion of extra premises. However, none can handle all these flexibilities simultaneously, resulting in missed relevant matches. In this work, we propose a type-based library search method based on equational unification modulo a set of type isomorphisms for dependent product/sum types, enabling all the desired search flexibilities. We present a semi-algorithm for this equational unification and provide a prototype implementation to demonstrate the feasibility of our approach.
@InProceedings{TyDe25p15,
author = {Satoshi Takimoto and Sosuke Moriguchi and Takuo Watanabe},
title = {Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {15-25},
doi = {10.1145/3759538.3759651},
year = {2025},
}
Publisher's Version
TyDe '25: "The Conatural Numbers Form ..."
The Conatural Numbers Form an Exponential Commutative Semiring
Szumi Xie and Viktor Bense
(Eötvös Loránd University, Hungary)
Conatural numbers are a coinductive type dual to the inductively defined natural numbers. The conatural numbers can represent all natural numbers and an extra element for infinity, this can be useful for representing the amount of steps taken by a possibly non-terminating program. We can define functions on conatural numbers by corecursion, however proof assistants such as Agda require the corecursive definitions to be guarded to make sure that they are productive. This requirement is often too restrictive, as it disallows the corecursive occurrence to appear under previously defined operations. In this paper, we explore some methods to solving this issue using the running examples of multiplication and the commutativity of addition on conatural numbers, then we give comparisons between these methods. As the main result, this is the first proof that conatural numbers form an exponential commutative semiring in cubical type theory without major extensions.
@InProceedings{TyDe25p52,
author = {Szumi Xie and Viktor Bense},
title = {The Conatural Numbers Form an Exponential Commutative Semiring},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {52-63},
doi = {10.1145/3759538.3759654},
year = {2025},
}
Publisher's Version