Powered by
7th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2022),
September 11, 2022,
Ljubljana, Slovenia
7th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2022)
Frontmatter
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
(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.
@InProceedings{TyDe22p1,
author = {Zilin Chen},
title = {A Hoare Logic Style Refinement Types Formalisation},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--14},
doi = {10.1145/3546196.3550162},
year = {2022},
}
Publisher's Version
Structural Refinement Types
David Binder,
Ingo Skupin,
David Läwen, and
Klaus Ostermann
(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.
@InProceedings{TyDe22p15,
author = {David Binder and Ingo Skupin and David Läwen and Klaus Ostermann},
title = {Structural Refinement Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {15--27},
doi = {10.1145/3546196.3550163},
year = {2022},
}
Publisher's Version
tylr: A Tiny Tile-Based Structure Editor
David Moon,
Andrew Blinn, and
Cyrus Omar
(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.
@InProceedings{TyDe22p28,
author = {David Moon and Andrew Blinn and Cyrus Omar},
title = {tylr: A Tiny Tile-Based Structure Editor},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {28--37},
doi = {10.1145/3546196.3550164},
year = {2022},
}
Publisher's Version
Computing with Generic Trees in Agda
Stephen Dolan
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.
@InProceedings{TyDe22p38,
author = {Stephen Dolan},
title = {Computing with Generic Trees in Agda},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {38--44},
doi = {10.1145/3546196.3550165},
year = {2022},
}
Publisher's Version
proc time: 0.82