Search

To design type systems that use subtyping, we have to make tradeoffs. Deep subtyping is more expressive than shallow subtyping, because deep subtyping compares the entire structure of types. However, shallow subtyping is easier to reason about. By eta-expanding source programs, we can get the effect of deep subtyping with less of its complexity. An early paper on filter models (Barendregt et al. 1983) examined two similar intersection type systems. The first included a subsumption rule that used a rich subtyping relation, including multiple rules for the top type and a distributivity rule. Their second type system dropped the subsumption rule, but added a rule that allowed a term to be eta-expanded before typing it. This rule in their second type system compensated for the lack of subsumption: where their first type system used subtyping to manipulate intersections deep inside types, their second type system used introduction and elimination rules directly on the subterms created by eta-expansion. Viewed as a computation, their proof of completeness for the second (shallow) system performs eta-expansion. Thus, we can regard their proof as inventing the application of eta-expansion to avoid deep subtyping. This paper serves as a tutorial on using eta-expansion to obviate deep subtyping, puts the invention of the technique by Barendregt et al. (1983) into context, gives a complete proof of the relevant lemma, and discusses how the technique can be used in type system design., Comment: 16 pages, 8 figures

We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization., Comment: 61 pages + appendix with proofs, Just Accepted version of paper (with new title) at ACM Transactions on Programming Languages and Systems

Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner's local type inference to the present day, and provide guidance for future investigations., Comment: 37 pages; submitted to ACM Computing Surveys

Incremental computations attempt to exploit input similarities over time, reusing work that is unaffected by input changes. To maximize this reuse in a general-purpose programming setting, programmers need a mechanism to identify dynamic allocations (of data and subcomputations) that correspond over time. We present Fungi, a typed functional language for incremental computation with names. Unlike prior general-purpose languages for incremental computing, Fungi's notion of names is formal, general, and statically verifiable. Fungi's type-and-effect system permits the programmer to encode (program-specific) local invariants about names, and to use these invariants to establish global uniqueness for their composed programs, the property of using names correctly. We prove that well-typed Fungi programs respect global uniqueness. We derive a bidirectional version of the type and effect system, and we have implemented a prototype of Fungi in Rust. We apply Fungi to a library of incremental collections, showing that it is expressive in practice.

Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes. Existing type systems for datasort refinements require that all the refinements of a type be specified when the type is declared; multiple refinements of the same type can be obtained only by duplicating type definitions, and consequently, duplicating code. We enrich the traditional notion of a signature, which describes the inhabitants of datasorts, to allow re-refinement via signature extension, without duplicating definitions. Since arbitrary updates to a signature can invalidate the inversion principles used to check case expressions, we develop a definition of signature well-formedness that ensures that extensions maintain existing inversion principles. This definition allows different parts of a program to extend the same signature in different ways, without conflicting with each other. Each part can be type-checked independently, allowing separate compilation., Comment: 27 pages + 26 page appendix, to appear at ESOP 2017

A long-standing shortcoming of statically typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types distinguish different values of datatypes; if a program annotated with refinements passes type checking, pattern-matching failures become impossible. Unfortunately, refinement is a monolithic property of a type, exacerbating the difficulty of adding refinement types to nontrivial programs. Gradual typing has explored how to incrementally move between static typing and dynamic typing. We develop a type system of gradual sums that combines refinement with imprecision. Then, we develop a bidirectional version of the type system, which rules out excessive imprecision, and give a type-directed translation to a target language with explicit casts. We prove that the static sublanguage cannot have match failures, that a well-typed program remains well-typed if its type annotations are made less precise, and that making annotations less precise causes target programs to fail later. Several of these results correspond to criteria for gradual typing given by Siek et al. (2015)., Comment: 14 pages + appendix with proofs, to appear at POPL 2017

Many programming language techniques for incremental computation employ programmer-specified names for cached information. At runtime, each name identifies a "cache location" for a dynamic data value or a sub-computation; in sum, these cache location choices guide change propagation and incremental (re)execution. We call a cache location name precise when it identifies at most one value or subcomputation; we call all other names imprecise, or ambiguous. At a minimum, cache location names must be precise to ensure that change propagation works correctly; yet, reasoning statically about names in incremental programs remains an open problem. As a first step, this paper defines and solves the precise name problem, where we verify that incremental programs with explicit names use them precisely. To do so, we give a refinement type and effect system, and prove it sound (every well-typed program uses names precisely). We also demonstrate that this type system is expressive by verifying example programs that compute over efficient representations of incremental sequences and sets. Beyond verifying these programs, our type system also describes their dynamic naming strategies, e.g., for library documentation purposes.

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its applicability to a variety of type systems, its error reporting, and its ease of implementation. Following principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to indexed types (generalized algebraic datatypes) are less clear. Building on proof-theoretic treatments of equality, we give a declarative specification of typing based on focalization. This approach permits declarative rules for coverage of pattern matching, as well as support for first-class existential types using a focalized subtyping judgment. We use refinement types to avoid explicitly passing equality proofs in our term syntax, making our calculus similar to languages such as Haskell and OCaml. We also extend the declarative specification with an explicit rules for deducing when a type is principal, permitting us to give a complete declarative specification for a rich type system with significant type inference. We also give a set of algorithmic typing rules, and prove that it is sound and complete with respect to the declarative system. The proof requires a number of technical innovations, including proving soundness and completeness in a mutually recursive fashion., Comment: 28 pages, plus lemmas and proofs (191 pages); accepted to POPL 2019

We classify programming languages according to evaluation order: each language fixes one evaluation order as the default, making it transparent to program in that evaluation order, and troublesome to program in the other. This paper develops a type system that is impartial with respect to evaluation order. Evaluation order is implicit in terms, and explicit in types, with by-value and by-name versions of type connectives. A form of intersection type quantifies over evaluation orders, describing code that is agnostic over (that is, polymorphic in) evaluation order. By allowing such generic code, programs can express the by-value and by-name versions of a computation without code duplication. We also formulate a type system that only has by-value connectives, plus a type that generalizes the difference between by-value and by-name connectives: it is either a suspension (by name) or a "no-op" (by value). We show a straightforward encoding of the impartial type system into the more economical one. Then we define an elaboration from the economical language to a call-by-value semantics, and prove that elaborating a well-typed source program, where evaluation order is implicit, produces a well-typed target program where evaluation order is explicit. We also prove a simulation between evaluation of the target program and reductions (either by-value or by-name) in the source program. Finally, we prove that typing, elaboration, and evaluation are faithful to the type annotations given in the source program: if the programmer only writes by-value types, no by-name reductions can occur at run time., Comment: 13 pages + appendix; in International Conference on Functional Programming (ICFP) 2015. arXiv version 3 makes corrections to Figure 5 and Section 2.4, preserving page breaks

Over the past thirty years, there has been significant progress in developing general-purpose, language-based approaches to incremental computation, which aims to efficiently update the result of a computation when an input is changed. A key design challenge in such approaches is how to provide efficient incremental support for a broad range of programs. In this paper, we argue that first-class names are a critical linguistic feature for efficient incremental computation. Names identify computations to be reused across differing runs of a program, and making them first class gives programmers a high level of control over reuse. We demonstrate the benefits of names by presenting NOMINAL ADAPTON, an ML-like language for incremental computation with names. We describe how to use NOMINAL ADAPTON to efficiently incrementalize several standard programming patterns -- including maps, folds, and unfolds -- and show how to build efficient, incremental probabilistic trees and tries. Since NOMINAL ADAPTON's implementation is subtle, we formalize it as a core calculus and prove it is from-scratch consistent, meaning it always produces the same answer as simply re-running the computation. Finally, we demonstrate that NOMINAL ADAPTON can provide large speedups over both from-scratch computation and ADAPTON, a previous state-of-the-art incremental computation system., Comment: OOPSLA '15, October 25-30, 2015, Pittsburgh, PA, USA

In functional programming languages, the classic form of annotation is a single type constraint on a term. Intersection types add complications: a single term may have to be checked several times against different types, in different contexts, requiring annotation with several types. Moreover, it is useful (in some systems, necessary) to indicate the context in which each such type is to be used. This paper explores the technical design space of annotations in systems with intersection types. Earlier work (Dunfield and Pfenning 2004) introduced contextual typing annotations, which we now tease apart into more elementary mechanisms: a "right hand" annotation (the standard form), a "left hand" annotation (the context in which a right-hand annotation is to be used), a merge that allows for multiple annotations, and an existential binder for index variables. The most novel element is the left-hand annotation, which guards terms (and right-hand annotations) with a judgment that must follow from the current context., Comment: In Proceedings ITRS 2012, arXiv:1307.7849

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type systems), its error reporting, and its relative ease of implementation. Following design principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to polymorphism, however, are less obvious. We give a declarative, bidirectional account of higher-rank polymorphism, grounded in proof theory; this calculus enjoys many properties such as eta-reduction and predictability of annotations. We give an algorithm for implementing the declarative system; our algorithm is remarkably simple and well-behaved, despite being both sound and complete., Comment: 13 pages + 78-page appendix, to appear in International Conference on Functional Programming (ICFP) 2013

Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume many different features. In modern type systems, parametric polymorphism is fundamental, but intersection polymorphism has gained little traction in programming languages. Most practical intersection type systems have supported only refinement intersections, which increase the expressiveness of types (more precise properties can be checked) without altering the expressiveness of terms; refinement intersections can simply be erased during compilation. In contrast, unrestricted intersections increase the expressiveness of terms, and can be used to encode diverse language features, promising an economy of both theory and implementation. We describe a foundation for compiling unrestricted intersection and union types: an elaboration type system that generates ordinary lambda-calculus terms. The key feature is a Forsythe-like merge construct. With this construct, not all reductions of the source program preserve types; however, we prove that ordinary call-by-value evaluation of the elaborated program corresponds to a type-preserving evaluation of the source program. We also describe a prototype implementation and applications of unrestricted intersections and unions: records, operator overloading, and simulating dynamic typing., Comment: 13 pages, 12 figures, to appear in International Conference on Functional Programming (ICFP) 2012

Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics. Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into let-normal form drastically reduces the number of choices. The key results are soundness and completeness: a typing derivation (in the system with too many subterm choices) exists for a program if and only if a derivation exists for the let-normalized program., Comment: In Proceedings ITRS 2010, arXiv:1101.4104