Functional
Temporal Higher Order Contracts
Tim Disney, Cormac Flanagan, Jay McCarthy
2011
Behavioral contracts are embraced by software engineers because they document module interfaces, detect interface violations, and help identify faulty modules (packages, classes, functions, etc). This paper extends prior higherorder contract systems to also express and enforce temporal properties, which are common in software systems with imperative state, but which are mostly left implicit or are at best informally specified. The paper presents both a programmatic contract API as well as a temporal contract language, and reports on experience and performance results from implementing these contracts in Racket.
Our development formalizes module behavior as a trace of events such as function calls and returns. Our contract system provides both noninterference (where contracts cannot influence correct executions) and also a notion of completeness (where contracts can enforce any decidable, prefixclosed predicate on event traces).
This paper appears to be about a way to define (and enforce through dynamic monitoring) correctness properties of APIs by enforcing or ruling out certain orderings of function calls, such as calling a "read" method on a file descriptor after having called "close". I am personally not convinced that this specification language is a good way to solve these problems. However, the bulk of the paper is actually about giving a denotational semantics to contracts, as specifying a set of traces that the external interface of a component may expose (in a way strongly reminding of game semantics), and this feels like an important technique to reason about contracts. The exposition of this contribution is practical (based on a simple abstract machine) and accessible.
Designers of Elm want their compiler to produce friendly error messages. They show some examples of helpful error messages from their newer compiler on the blog post.
Compilers as Assistants
One of Elm’s goals is to change our relationship with compilers. Compilers should be assistants, not adversaries. A compiler should not just detect bugs, it should then help you understand why there is a bug. It should not berate you in a robot voice, it should give you specific hints that help you write better code. Ultimately, a compiler should make programming faster and more fun!
Breaking Through the Normalization Barrier: A SelfInterpreter for Fomega, by Matt Brown and Jens Palsberg:
According to conventional wisdom, a selfinterpreter for a strongly normalizing λcalculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a selfinterpreter for System Fω, a strongly normalizing λcalculus. After a careful analysis of the classical theorem, we show that static type checking in Fω can exclude the proof’s diagonalization gadget, leaving open the possibility for a selfinterpreter. Along with the selfinterpreter, we program four other operations in Fω, including a continuationpassing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.
I haven't gone through the whole paper, but their claims are compelling. They have created selfinterpreters in System F, System Fω and System Fω+, which are all strongly normalizing typed languages. Previously, the only instance of this for a typed language was Girard's System U, which is not strongly normalizing. The key lynchpin appears in this paragraph on page 2:
Our result breaks through the normalization barrier. The conventional wisdom underlying the normalization barrier makes an implicit assumption that all representations will behave like their counterpart in the computability theorem, and therefore the theorem must apply to them as well. This assumption excludes other notions of representation, about which the theorem says nothing. Thus, our result does not contradict the theorem, but shows that the theorem is less farreaching than previously thought.
Pretty cool if this isn't too complicated in any given language. Could let one move some previously nontypesafe runtime features, into type safe libraries.
Optimizing Closures in O(0) time, by Andrew W. Keep, Alex Hearn, R. Kent Dybvig:
The flatclosure model for the representation of firstclass procedures is simple, safeforspace, and efficient, allowing the values or locations of free variables to be accessed with a single memory indirect. It is a straightforward model for programmers to understand, allowing programmers to predict the worstcase behavior of their programs. This paper presents a set of optimizations that improve upon the flatclosure model along with an algorithm that implements them, and it shows that the optimizations together eliminate over 50% of runtime closurecreation and freevariable access overhead in practice, with insignificant compiletime overhead. The optimizations never add overhead and remain safeforspace, thus preserving the benefits of the flatclosure model.
Looks like a nice and simple set of optimizations for probably the most widely deployed closure representation.
The Royal Society will award Xavier Leroy the Milner Award 2016
... in recognition of his research on the OCaml functional programming language and on the formal verification of compilers.
Xavier's replied:
It is very moving to see how far we have come, from Milner's great ideas of the 1970s to tools as powerful and as widely used as OCaml and Coq.
Freer Monads, More Extensible Effects, by Oleg Kiselyov and Hiromi Ishii:
We present a rational reconstruction of extensible effects, the recently proposed alternative to monad transformers, as the confluence of efforts to make effectful computations compose. Free monads and then extensible effects emerge from the straightforward term representation of an effectful computation, as more and more boilerplate is abstracted away. The generalization process further leads to freer monads, constructed without the Functor constraint.
The continuation exposed in freer monads can then be represented as an efficient typealigned data structure. The end result is the algorithmically efficient extensible effects library, which is not only more comprehensible but also faster than earlier implementations. As an illustration of the new library, we show three surprisingly simple applications: nondeterminism with committed choice (LogicT), catching IO exceptions in the presence of other effects, and the semiautomatic management of file handles and other resources through monadic regions.
We extensively use and promote the new sort of ‘laziness’, which underlies the left Kan extension: instead of performing an operation, keep its operands and pretend it is done.
This looks very promising, and includes some benchmarks comparing the heavily optimized and specialcased monad transformers against this new formulation of extensible effects using Freer monads.
See also the reddit discussion.
Reagents: Expressing and Composing Finegrained Concurrency, by Aaron Turon:
Efficient communication and synchronization is crucial for finegrained parallelism. Libraries providing such features, while indispensable, are difficult to write, and often cannot be tailored or composed to meet the needs of specific users. We introduce reagents, a set of combinators for concisely expressing concurrency algorithms. Reagents scale as well as their handcoded counterparts, while providing the composability existing libraries lack.
This is a pretty neat approach to writing concurrent code, which lies somewhere between manually implementing lowlevel concurrent algorithms and STM. Concurrent algorithms are expressed and composed seminaively, and Reagents automates the retries for you in case of thread interference (for transient failure of CAS updates), or they block waiting for input from another thread (in case of permanent failure where no input is available).
The core seems to be kCAS with synchronous communication between threads to coordinate reactions on shared state. The properties seem rather nice, as Aaron describes:
When used in isolation, reagents are guaranteed to perform only the CASes that the handwritten algorithm would, so they introduce no overhead on sharedmemory operations; by recoding an algorithm use reagents, you lose nothing. Yet unlike handwritten algorithms, reagents can be composed using choice, tailored with new blocking behavior, or combined into larger atomic blocks.
The benchmarks in section 6 look promising. This appears to be work towards Aaron's thesis which provides many more details.
Interesting survey.
Based on a brief look I am not sure I agree with all the conclusions/rankings. But most seem to make sense and the Notable Libraries and examples in each category are helpful.
Don Syme receives the Royal Academy of Engineering's Silver Medal for his work on F#. The citation reads:
F# is known for being a clear and more concise language that interoperates well with other systems, and is used in applications as diverse asanalysing the UK energy market to tackling money laundering. It allows programmers to write code with fewer bugs than other languages, so users can get their programme delivered to market both rapidly and accurately. Used by major enterprises in the UK and worldwide, F# is both crossplatform and open source, and includes innovative features such as unitofmeasure inference, asynchronous programming and type providers, which have in turn influenced later editions of C# and other industry languages.
Congratulations!
SelfRepresentation in Girard’s System U, by Matt Brown and Jens Palsberg:
In 1991, Pfenning and Lee studied whether System F could support a typed selfinterpreter. They concluded that typed selfrepresentation for System F “seems to be impossible”, but were able to represent System F in Fω. Further, they found that the representation of Fω requires kind polymorphism, which is outside Fω. In 2009, Rendel, Ostermann and Hofer conjectured that the representation of kindpolymorphic terms would require another, higher form of polymorphism. Is this a case of infinite regress?
We show that it is not and present a typed selfrepresentation for Girard’s System U, the first for a λcalculus with decidable type checking. System U extends System Fω with kind polymorphic terms and types. We show that kind polymorphic types (i.e. types that depend on kinds) are sufficient to “tie the knot” – they enable representations of kind polymorphic terms without introducing another form of polymorphism. Our selfrepresentation supports operations that iterate over a term, each of which can be applied to a representation of itself. We present three typed selfapplicable operations: a selfinterpreter that recovers a term from its representation, a predicate that tests the intensional structure of a term, and a typed continuationpassingstyle (CPS) transformation – the first typed selfapplicable CPS transformation. Our techniques could have applications from verifiably typepreserving metaprograms, to growable typed languages, to more efficient selfinterpreters.
Typed selfrepresentation has come up here on LtU in the past. I believe the best selfinterpreter available prior to this work was a variant of Barry Jay's SFcalculus, covered in the paper Typed SelfInterpretation by Pattern Matching (and more fully developed in Structural Types for the Factorisation Calculus). These covered statically typed selfinterpreters without resorting to undecidable type:type rules.
However, being combinator calculi, they're not very similar to most of our programming languages, and so selfinterpretation was still an active problem. Enter Girard's System U, which features a more familiar type system with only kind * and kindpolymorphic types. However, System U is not strongly normalizing and is inconsistent as a logic. Whether selfinterpretation can be achieved in a strongly normalizing language with decidable type checking is still an open problem.

Recent comments
6 hours 48 min ago
8 hours 5 min ago
10 hours 51 min ago
2 days 9 hours ago
2 days 13 hours ago
2 days 14 hours ago
3 days 1 hour ago
3 days 1 hour ago
3 days 9 hours ago
3 days 10 hours ago