Destination passing —aka. out parameters— is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant.

A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. This paper presents linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are filled in automatically by the compiler. We present linear constraints as a qualified type system,together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.

Union and intersection types are a staple of gradually typed languages such as TypeScript. While it's long been recognized that union and intersection types are difficult to verify statically, it may appear at first that the dynamic part of gradual typing is actually pretty simple.

A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages have traditionally been ill-equipped to embed this sort of languages. The Arrow abstraction is an approximation, but we argue that it does not capture the right properties.

Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to function arrows . Linear functions can receive inputs from linearly-bound values, but can also operate over unrestricted, regular values. To demonstrate the efficacy of our linear type system — both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types — we implemented our type system in ghc, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I/O-performing functions.

In the context of statically typed, class-based languages , we investigate classes that can be extended with trait composition. A trait is a collection of methods without state; it can be viewed as an incomplete stateless class . Traits can be composed in any order, but only make sense when imported by a class that provides state variables and additional methods to disambiguate conflicting names arising between the imported traits. We introduce FeatherTrait Java (FTJ), a conservative extension of the simple lightweight class-based calculus Featherweight Java (FJ) with statically typed traits . In FTJ, classes can be built using traits as basic behavioral bricks; method conflicts between imported traits must be resolved explicitly by the user either by (i) aliasing or excluding method names in traits, or by (ii) overriding explicitly the conflicting methods in the class or in the trait itself. We present an operational semantics with a lookup algorithm, and a sound type system that guarantees that evaluating a well-typed expression never yields a message-not-understood run-time error nor gets the interpreter stuck. We give examples of the increased expressive power of the trait-based inheritance model. The resulting calculus appears to be a good starting point for a rigorous mathematical analysis of typed class-based languages featuring trait-based inheritance.

Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain interpretation of type theory one can in turn simplify further U. Berger's argument. We build a domain model for an untyped programming language where U. Berger has an interpretation only for typed terms or alternatively has an interpretation for untyped terms but need an extra condition to deduce strong normalisation. As a main application, we show that Martin-L\"{o}f dependent type theory extended with a program for Spector double negation shift.

U. Bergel; [ I I ] signijicantly simplijied Tait's normalisation proof for bar recursion [27], see also [9], replacing Tait's introduction of injinite terms by the construction of a domain having the property that a term is strongly normalizing if its semantics is \ne. The goal of this paper is to show that, using ideas from the theory of intersection types [2, 6, 7, 211 and Martin-Liif's domain interpretation of type theory [18], we can in turn simplify U. Berger's argument in the construction of such a domain model. We think that our domain model can be used to give modular proofs of strong normalization for various type theory. As an example, we show in some details how it can be used to prove strong normalization for Martin-Liif dependent type theory extended with bar recursion, and with some form ofproof-irrelevance.