TyDe '25: Proceedings of the 10th ACM SIGPLAN International Workshop on Type-Driven Development

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.

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.

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.

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.

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.