ICFP Workshops 2023
28th ACM SIGPLAN International Conference on Functional Programming (ICFP 2023)
Powered by
Conference Publishing Consulting

8th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2023), September 4, 2023, Seattle, WA, USA

TyDe 2023 – Proceedings

Contents - Abstracts - Authors

8th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2023)


Title Page

Welcome from the Chairs
Welcome to the 8th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2023), co-located with the International Conference on Functional Programming (ICFP 2023). The workshop brings together leading researchers and practitioners who are using or exploring types as a means to support program development.
Historically, TyDe is a merging of two previous workshops: the Workshop on Dependently Typed Programming and the Workshop on Generic Programming. These two research areas have a rich history, bridging both theory and practice, and having types at their core. Novel techniques explored by both communities have gradually spread to more mainstream languages. This workshop thus covers topics of generic programming and dependently typed programming, as well as static and dynamic analyses of types, tools and IDEs, and generally the design and implementation of programming languages exploiting types in novel ways. The workshop features contributions from around the world capturing the state of the art in these important areas.
The call for submissions sought both full papers (up to 12 pages, published in the ACM Digital Library) and extended abstracts (up to 3 pages, not formally published but posted on the workshop webpage). Each submission was evaluated by 2--3 members of the program committee: full papers for the novelty and significance of their results, and extended abstracts for relevance and interest to the TyDe community. We received 7 full papers and 8 extended abstracts, of which 5 and 7 respectively were accepted. We also had a keynote talk by Jeremy Gibbons of the University of Oxford.
We would like to express our thanks to the contributors, the program committee members, the external reviewers, the TyDe steering committee, and the organizers of ICFP 2023.

TyDe 2023 Organization


A Calculus of Inductive Linear Constructions
Qiancheng Fu ORCID logo and Hongwei Xi ORCID logo
(Boston University, USA)
In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode in a straightforward manner the linear connectives that must be baked into the core of other systems. This greatly lowers the difficulty of encoding various data structures and makes writing non-trivial programs humanly feasible. We study the standard meta theory of our calculus, showing that it is sound in the usual sense. Through a heap-based operational semantics, we show that CILC safely manipulates resources and runs memory clean. We have formalized and proven correct most of the reported results in the Coq Proof Assistant.

Publisher's Version Published Artifact Artifacts Available
Semantic Encapsulation using Linking Types
Daniel Patterson ORCID logo, Andrew Wagner ORCID logo, and Amal AhmedORCID logo
(Northeastern University, USA)
Interoperability pervades nearly all mainstream language implementations, as most systems leverage subcomponents written in different languages. And yet, such linking can expose a language to foreign behaviors that are internally inexpressible, which poses a serious threat to safety invariants and programmer reasoning. To preserve such invariants, a language may try to add features to limit the reliance on external libraries, but endless extensions can obscure the core abstractions the language was designed to provide.
In this paper, we outline an approach that encapsulates foreign code in a sound way—i.e., without disturbing the invariants promised by types of the core language. First, one introduces novel linking types that characterize the behaviors of foreign libraries that are inexpressible in the core language. To reason about the soundness of linking, one constructs a realizability model that captures the meaning of both core types and linking types as sets of target-language terms. Using this model, one can formally prove when foreign behavior is encapsulated; that is, unobservable to core code. We show one way to discharge such proofs automatically by augmenting the compiler to insert verified encapsulation wrappers around components that use foreign libraries.
Inspired by existing approaches to FFIs, we develop a pair of case studies that extend a pure, functional language: one extension for state, and another for exceptions. The first allows us to implement mutable references via a library, whereas the second allows us to implement try and catch as library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.

Publisher's Version
Infix-Extensible Record Types for Tabular Data
Adam Paszke ORCID logo and Ningning Xie ORCID logo
(Google DeepMind, Germany; Google DeepMind, Canada)
We present a novel row-polymorphic record calculus, supporting a unique combination of features: scoped labels, first-class labels and rows, and record concatenation. Our work is motivated by the similarity of record types and data table (or data frame) schemas, commonly used in data processing tasks. After presenting our record calculus, we demonstrate its applicability to data frame manipulation by showing that it can be used to successfully assign types to the functions listed in the Brown Benchmark for Tabular Types. Our typing discipline is remarkably lightweight, compared to calculi that require reasoning about type-level constraints when manipulating record types, making it a viable candidate for practical use.

Publisher's Version
A Dependently Typed Language with Dynamic Equality
Mark Lemay ORCID logo, Qiancheng Fu ORCID logo, William Blair ORCID logo, Cheng Zhang ORCID logo, and Hongwei Xi ORCID logo
(Autodesk, USA; Boston University, USA)
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.

Publisher's Version
Combining Dependency, Grades, and Adjoint Logic
Peter Hanukaev ORCID logo and Harley Eades III ORCID logo
(Augusta University, USA)
We propose two new dependent type systems. The first, is a dependent graded/linear type system where a graded dependent type system is connected via modal operators to a linear type system in the style of Linear/Non-linear logic. We then generalize this system to support many graded systems connected by many modal operators through the introduction of modes from Adjoint Logic. Finally, we prove several meta-theoretic properties of these two systems including graded substitution.

Publisher's Version

proc time: 2.22