TyDe 2022: Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development

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.

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.

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.

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.