Type Theory
Philip Wadler posts his exchange with William Howard on history of the CurryHoward correspondence. Howard on CurryHoward.
Type soundness and freedom for Mezzo,
Thibaut Balabonski, François Pottier, and Jonathan Protzenko,
2014
Full paper
Presentation slides
The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We incorporate sharedmemory concurrency into Mezzo and present a modular formalization of its core type system, in the form of a concurrent λcalculus, which we extend with references and locks. We prove that welltyped programs do not go wrong and are datarace free. Our definitions and proofs are machinechecked.
The Mezzo programming language has been mentioned recently on LtU. The article above is however not so much about the practice of Mezzo or justification of its design choices (for this, see Programming with Permissions in Mezzo, François Pottier and Jonathan Protzenko, 2013), but a presentation of its soundness proof.
I think this paper is complementary to more practiceoriented ones, and remarkable for at least two reasons:
 It is remarkably simple, for a complete soundness proof (and racefreeness) of a programming language with higherorder functions, mutable states, strong update, linear types, and dynamic borrowing. This is one more confirmation of the simplifying effect of mechanized theorem proving.
 It is the first soundness proof of a programming language that is strongly inspired by Separation Logic. (Concurrent) Separation Logic has been a revolution in the field of programming logics, but it had until now not be part of a fullfledged language design, and this example is bound to be followed by many others. I expect the structure of this proof to be reused many times in the future.
Backpack: Retrofitting Haskell with Interfaces
Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones, Simon Marlow
2014
Module systems like that of Haskell permit only a weak form of modularity in which module implementations directly depend on other implementations and must be processed in dependency order. Module systems like that of ML, on the other hand, permit a stronger form of modularity in which explicit interfaces express assumptions about dependencies, and each module can be typechecked and reasoned about independently.
In this paper, we present Backpack, a new language for building separatelytypecheckable packages on top of a weak module system like Haskell's. The design of Backpack is inspired by the MixML module calculus of Rossberg and Dreyer, but differs significantly in detail. Like MixML, Backpack supports explicit interfaces and recursive linking. Unlike MixML, Backpack supports a more flexible applicative semantics of instantiation. Moreover, its design is motivated less by foundational concerns and more by the practical concern of integration into Haskell, which has led us to advocate simplicity—in both the syntax and semantics of Backpack—over raw expressive power. The semantics of Backpack packages is defined by elaboration to sets of Haskell modules and binary interface files, thus showing how Backpack maintains interoperability with Haskell while extending it with separate typechecking. Lastly, although Backpack is geared toward integration into Haskell, its design and semantics are largely agnostic with respect to the details of the underlying core language.
Pure Subtype Systems, by DeLesley S. Hutchins:
This paper introduces a new approach to type theory called pure subtype systems. Pure subtype systems differ from traditional approaches to type theory (such as pure type systems) because the theory is based on subtyping, rather than typing. Proper types and typing are completely absent from the theory; the subtype relation is defined directly over objects. The traditional typing relation is shown to be a special case of subtyping, so the loss of types comes without any loss of generality.
Pure subtype systems provide a uniform framework which seamlessly integrates subtyping with dependent and singleton types. The framework was designed as a theoretical foundation for several problems of practical interest, including mixin modules, virtual classes, and featureoriented programming.
The cost of using pure subtype systems is the complexity of the metatheory. We formulate the subtype relation as an abstract reduction system, and show that the theory is sound if the underlying reductions commute. We are able to show that the reductions commute locally, but have thus far been unable to show that they commute globally. Although the proof is incomplete, it is “close enough” to rule out obvious counterexamples. We present it as an open problem in type theory.
A thoughtprovoking take on type theory using subtyping as the foundation for all relations. He collapses the type hierarchy and unifies types and terms via the subtyping relation. This also has the sideeffect of combining type checking and partial evaluation. Functions can accept "types" and can also return "types".
Of course, it's not all sunshine and roses. As the abstract explains, the metatheory is quite complicated and soundness is still an open question. Not too surprising considering type checking Type:Type is undecidable.
Hutchins' thesis is also available for a more thorough treatment. This work is all in pursuit of Hitchens' goal of featureoriented programming.
Types for Flexible Objects, by Pottayil Harisanker Menon, Zachary Palmer, Alexander Rozenshteyn, Scott Smith:
Scripting languages are popular in part due to their extremely flexible objects. These languages support numerous object features, including dynamic extension, mixins, traits, and ﬁrstclass messages. While some work has succeeded in typing these features individually, the solutions have limitations in some cases and no project has combined the results.
In this paper we deﬁne TinyBang, a small typed language containing only functions, labeled data, a data combinator, and pattern matching. We show how it can directly express all of the aforementioned ﬂexible object features and still have sound typing. We use a subtype constraint type inference system with several novel extensions to ensure full type inference; our algorithm reﬁnes parametric polymorphism for both flexibility and efficiency. We also use TinyBang to solve an open problem in OO literature: objects can be extended after being messaged without loss of width or depth subtyping and without dedicated metatheory. A core subset of TinyBang is proven sound and a preliminary implementation has been constructed.
An interesting paper I stumbled across quite by accident, it purports quite an ambitious set of features: generalizing previous work on firstclass cases while supporting subtyping, mutation, and polymorphism all with full type inference, in an effort to match the flexibility of dynamically typed languages.
It does so by introducing a host of new concepts that are almostbutnotquite generalizations of existing concepts, like "onions" which are kind of a typeindexed extensible record, and "scapes" which are sort of a generalization of pattern matching cases.
Instead of approaching objects via a record calculus, they approach it using its dual as variant matching. Matching functions then have degenerate dependent types, which I first saw in the paper Type Inference for FirstClass Messages with MatchFunctions. Interesting aside, Scott Smith was a coauthor on this last paper too, but it isn't referenced in the "flexible objects" paper, despite the fact that "scapes" are "matchfunctions".
Overall, quite a dense and ambitous paper, but the resulting TinyBang language looks very promising and quite expressive. Future work includes making the system more modular, as it currently requires whole program compilation, and adding firstclass labels, which in past work has led to interesting results as well. Most work exploiting row polymorphism is particularly interesting because it supports efficient compilation to indexpassing code for both records and variants. It's not clear if onions and scapes are also amenable to this sort of translation.
Edit: a previous paper was published in 2012, A Practical, Typed Variant Object Model  Or, How to Stand On Your Head and Enjoy the View. BigBang is their language that provides syntactic sugar on top of TinyBang.
Edit 2: commas fixed, thanks!
Conor McBride gave an 8lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:
Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedentlytyped programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the “pattern functors” which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of “container”. We shall expose the doublelife containers lead as “interaction structures” describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductiverecursive definitions, and we use that power to build universes of dependent types.
The lecture notes, code, and video captures are available online.
As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging.
Extensible Effects  An Alternative to Monad Transformers, by Oleg Kiselyov, Amr Sabry and Cameron Swords:
We design and implement a library that solves the longstanding problem of combining effects without imposing restrictions on their interactions (such as static ordering). Effects arise from interactions between a client and an effect handler (interpreter); interactions may vary throughout the program and dynamically adapt to execution conditions. Existing code that relies on monad transformers may be used with our library with minor changes, gaining efficiency over long monad stacks. In addition, our library has greater expressiveness, allowing for practical idioms that are inefﬁcient, cumbersome, or outright impossible with monad transformers.
Our alternative to a monad transformer stack is a single monad, for the coroutinelike communication of a client with its handler. Its type reﬂects possible requests, i.e., possible effects of a computation. To support arbitrary effects and their combinations, requests are values of an extensible union type, which allows adding and, notably, subtracting summands. Extending and, upon handling, shrinking of the union of possible requests is reﬂected in its type, yielding a typeandeffect system for Haskell. The library is lightweight, generalizing the extensible exception handling to other effects and accurately tracking them in types.
A followup to Oleg's delimited continuation adaptation of Cartwright and Felleisen's work on Extensible Denotational Language Specifications, which is a promising alternative means of composing effects to the standard monad transformers.
This work embeds a userextensible effect EDSL in Haskell by encoding all effects into a single effect monad using a novel open union type and the continuation monad. The encoding is very similar to recent work on Algebraic Effects and Handlers, and closely resembles a typed clientserver interaction ala coroutines. This seems like a nice convergence of the topics covered in the algebraic effects thread and other recent work on effects, and it's more efficient than monad transformers to boot.
Ross Tate is calling for "Industry Endorsement" for his paper MixedSite Variance.
..this is an attempt to make industry experience admissible as evidence in academic settings, just like they do in industry settings.
Abstract:
Java introduced wildcards years ago. Wildcards were very expressive, and they were integral to updating the existing libraries to make use of generics. Unfortunately, wildcards were also complex and verbose, making them hard and inconvenient for programmers to adopt. Overall, while an impressive feature, wildcards are generally considered to be a failure. As such, many languages adopted a more restricted feature for generics, namely declarationsite variance, because designers believed its simplicity would make it easier for programmers to adopt. Indeed, declarationsite variance has been quite successful. However, it is also completely unhelpful for many designs, including many of those in the Java SDK. So, we have designed mixedsite variance, a careful combination of definitionsite and usesite variance that avoids the failings of wildcards. We have been working with JetBrains to put this into practice by incorporating it into the design of their upcoming language, Kotlin. Here we exposit our design, our rationale, and our experiences.
Mention of it is also at Jetbrain's Kotlin blog.
Dependent Types for JavaScript, by Ravi Chugh, David Herman, Ranjit Jhala:
We present Dependent JavaScript (DJS), a staticallytyped dialect of the imperative, objectoriented, dynamic language. DJS supports the particularly challenging features such as runtime typetests, higherorder functions, extensible objects, prototype inheritance, and arrays through a combination of nested reﬁnement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies. With our implementation of DJS, we demonstrate that the type system is expressive enough to reason about a variety of tricky idioms found in small examples drawn from several sources, including the popular book JavaScript: The Good Parts and the SunSpider benchmark suite.
Some good progress on inferring types for a very dynamic language. Explicit type declarations are placed in comments that start with "/*:".
/*: x∶Top → {ν ∣ite Num(x) Num(ν) Bool(ν)} */
function negate(x) {
if (typeof x == "number") { return 0  x; }
else { return !x; }
}
How OCaml type checker works  or what polymorphism and garbage collection have in common
There is more to HindleyMilner type inference than the Algorithm W. In 1988, Didier Rémy was looking to speed up the type inference in Caml and discovered an elegant method of type generalization. Not only it is fast, avoiding the scan of the type environment. It smoothly extends to catching of locallydeclared types about to escape, to typechecking of universals and existentials, and to implementing MLF.
Alas, both the algorithm and its implementation in the OCaml type checker are little known and little documented. This page is to explain and popularize Rémy's algorithm, and to decipher a part of the OCaml type checker. The page also aims to preserve the history of Rémy's algorithm.
The attraction of the algorithm is its insight into type generalization as dependency tracking  the same sort of tracking used in automated memory management such as regions and generational garbage collection. Generalization can be viewed as finding dominators in the typeannotated abstract syntax tree with edges for shared types. Fluet and Morrisett's type system for regions and MetaOCaml environment classifiers use the generalization of a type variable as a criterion of region containment. Uncannily, Rémy's algorithm views the region containment as a test if a type variable is generalizable.
As usual with Oleg, there's a lot going on here. Personally, I see parallels with "lambda with letrec" and "callbypushvalue," although making the connection with the latter takes some squinting through some of Levy's work other than his CBPV thesis. Study this to understand OCaml type inference and/or MLF, or for insights into region typing, or, as the title suggests, for suggestive analogies between polymorphism and garbage collection.

Recent comments
32 min 49 sec ago
1 hour 13 min ago
1 hour 20 min ago
3 hours 29 min ago
4 hours 50 min ago
6 hours 16 min ago
6 hours 19 min ago
11 hours 36 min ago
17 hours 6 min ago
21 hours 7 min ago