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

7th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2022), September 11, 2022, Ljubljana, Slovenia

TyDe 2022 – Proceedings

Contents - Abstracts - Authors

7th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2022)

Frontmatter

Title Page


Welcome from the Chairs
This report aggregates the full papers presented at the Workshop on Type-Driven Development (TyDe) to be hosted on September 11, 2022 in Ljubljana, Slovenia, co-located with ICFP, the 27th ACM SIGPLAN International Conference on Functional Programming
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.
In addition to the four full papers which you see in these proceedings, seven extended abstracts will be presented at the workshop.
Thanks in advance to all presenters, participants, members of the program committee, the TyDe steering committee, and the organizers of ICFP 2022.

Papers

A Hoare Logic Style Refinement Types Formalisation
Zilin Chen ORCID logo
(UNSW, Australia)
Refinement types is a lightweight yet expressive tool for specifying and reasoning about programs. The connection between refinement types and Hoare logic has long been recognised but the discussion remains largely informal. In this paper, we present a Hoare triple style Agda formalisation of a refinement type system on a simply-typed λ-calculus restricted to first-order functions. In our formalisation, we interpret the object language as shallow Agda terms and use Agda’s type system as the underlying logic for the type refinement. To deterministically typecheck a program with refinement types, we reduce it to the computation of the weakest precondition and define a verification condition generator which aggregates all the proof obligations that need to be fulfilled to witness the well-typedness of the program.

Publisher's Version
Structural Refinement Types
David BinderORCID logo, Ingo Skupin ORCID logo, David Läwen ORCID logo, and Klaus Ostermann ORCID logo
(University of Tübingen, Germany)
Static types are a great form of lightweight static analysis. But sometimes a type like List is too coarse – we would also like to work with its refinements like non-empty lists, or lists containing exactly 42 elements. Dependent types allow for this, but they impose a heavy proof burden on the programmer. We want the checking and inference of refinements to be fully automatic.
In this article we present a simple refinement type system and inference algorithm which uses only variants of familiar concepts from constraint-based type inference. Concretely, we build on the algebraic subtyping approach and extend it with typing rules which combine properties of nominal and structural type systems in a novel way. Despite the simplicity of our approach, the resulting type system is very expressive and allows to specify and infer non-trivial properties of programs.

Publisher's Version
tylr: A Tiny Tile-Based Structure Editor
David Moon ORCID logo, Andrew BlinnORCID logo, and Cyrus OmarORCID logo
(University of Michigan, USA)
Structure editors designed for keyboard input often struggle to resolve the tension between maintaining hierarchical term structure and offering efficient linear editing affordances. Contemporary designs either compromise structure by deferring to text near the leaves or else maintain structure by permitting only edits that transform the selected term. However, visually adjacent sequences (e.g. of operators, operands, and individual delimiters) do not always cleave cleanly to term boundaries, so even experienced users report difficulties with selection and code restructuring tasks. We propose a novel approach to structure editing, tile-based editing, that maintains term structure while offering linear selection and modification affordances. The idea is to allow disassembly of terms into linearly sequenced tiles and shards around user selections, while guiding the user through restructuring actions and automatically inserting holes in a manner that ensures reassembly into a term.
This paper introduces tylr, a tiny tile-based editor designed primarily to highlight this uniquely flexible set of affordances. We evaluated tylr with a lab study where participants performed simple code transcription and modification tasks using tylr as well as a text editor and a structure editor built on JetBrains MPS, a state-of-the-art keyboard-driven structure editor generator. Our results indicate that participants frequently made use of tylr’s selection expressivity, and that this flexibility helped them complete some modification tasks significantly more quickly than with the MPS editor. We further observed that a few participants completed some tasks more quickly using tylr than with text, but were in general slowed by a number of limitations in our current design and implementation. We discuss these limitations and suggest future research and design directions aiming toward more flexible structure editing interfaces.

Publisher's Version
Computing with Generic Trees in Agda
Stephen Dolan ORCID logo
Dependently-typed programming languages offer powerful new means of abstraction, allowing the programmer to work generically across data structures. However, using the standard generic encoding of tree-like data structures (the W-types), we soon notice a caveat: the computational behaviour of W-types does not quite match their first-order counterparts. Here, we show how a tweak to the definition of W-types avoids this caveat, making the generic definition work just as well as the direct one.

Publisher's Version

proc time: 3