In his blog, Bob Harper, in joint effort with Dave MacQueen and Lars Bergstrom, announces the launch of sml-family.org:
The Standard ML Family project provides a home for online versions of various formal definitions of Standard ML, including the "Definition of Standard ML, Revised" (Standard ML 97). The site also supports coordination between different implementations of the Standard ML (SML) programming language by maintaining common resources such as the documentation for the Standard ML Basis Library and standard test suites. The goal is to increase compatibility and resource sharing between Standard ML implementations.
The site includes a history section devoted to the history of ML, and of Standard ML in particular. This section will contain a collection of original source documents relating to the design of the language.
Logical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:
We present a complete polymorphic effect inference algorithm for an ML-style language with handlers of not only exceptions, but of any other algebraic effect such as input & output, mutable references and many others. Our main aim is to offer the programmer a useful insight into the effectful behaviour of programs. Handlers help here by cutting down possible effects and the resulting lengthy output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred information from the programmer.
Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial.
Breaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures by Pieter Wuille and Tom Schrijvers:
Pure functional programming language offer many advantages over impure languages. Unfortunately, the absence of destructive update, imposes a complexity barrier. In imperative languages, there are algorithms and data structures with better complexity. We present our project for combining existing program transformation techniques to transform inefficient pure data structures into impure ones with better complexity. As a consequence, the programmer is not exposed to the impurity and retains the advantages of purity.
This paper is along the same lines a question I asked a couple of years ago. The idea here is to allow programming using immutable interfaces, and then automatically transform it into a more efficient mutable equivalent.
Earlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Luca Cardelli has made exceptional contributions to the world of programming
languages and beyond. Throughout his career, he has re-invented himself every
decade or so, while continuing to make true innovations. His achievements span
many areas: software; language design, including experimental languages;
programming language foundations; and the interaction of programming languages
and biology. These achievements form the basis of his lasting scientific leadership
and his wide impact.
Luca is always asking "what is new", and is always looking to
the future. Therefore, we have asked authors to produce short pieces that would
indicate where they are today and where they are going. Some of the resulting
pieces are short scientific papers, or abridged versions of longer papers; others are
less technical, with thoughts on the past and ideas for the future. We hope that
they will all interest Luca.
Hopefully the videos will be posted soon.
Propositions as Types, Philip Wadler. Draft, March 2014.
The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery.
Philip Wadler has written a very enjoyable (Like busses: you wait two thousand years for a definition of â€œeffectively calculableâ€, and then three come along at once) paper about propositions as types that is accessible to PLTlettantes.
CK Hur, D Dreyer, G Neis, V Vafeiadis (POPL 2012). The marriage of bisimulations and Kripke logical relations
There has been great progress in recent years on developing effective
techniques for reasoning about program equivalence in ML-like
languages---that is, languages that combine features like higher-order
functions, recursive types, abstract types, and general mutable
references. Two of the most prominent types of techniques to have
emerged are bisimulations and Kripke logical relations (KLRs).
While both approaches are powerful, their complementary advantages
have led us and other researchers to wonder whether there is an
essential tradeoff between them. Furthermore, both approaches seem to
suffer from fundamental limitations if one is interested in scaling
them to inter-language reasoning.
In this paper, we propose relation transition systems (RTSs), which
marry together some of the most appealing aspects of KLRs and
bisimulations. In particular, RTSs show how bisimulations' support
for reasoning about recursive features via coinduction can be
synthesized with KLRs' support for reasoning about local state via
state transition systems. Moreover, we have designed RTSs to avoid
the limitations of KLRs and bisimulations that preclude their
generalization to inter-language reasoning. Notably, unlike KLRs,
RTSs are transitively composable.
I understand the paper as offering an extension to bisimulation that handles the notion of hidden transitions properly and so allows a generalisation of KLRs to any systems that can be treated using bisimulations. Applications to verified compilation are mentioned, and everything has been validated in Coq.
Andreas Abel and Brigitte Pientka's Well-Founded
Recursion with Copatterns; a Unified Approach to Termination and
Productivity is one of my highlights of the just-finished ICFP
2013, but it makes sense to focus on the first paper on this work,
published at POPL back in January.
Copatterns: Programming Infinite Structures by Observations
Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer
Inductive datatypes provide mechanisms to define finite data such as
finite lists and trees via constructors and allow programmers to
analyze and manipulate finite data via pattern matching. In this
paper, we develop a dual approach for working with infinite data
structures such as streams. Infinite data inhabits coinductive
datatypes which denote greatest fixpoints. Unlike finite data which is
defined by constructors we define infinite data by observations. Dual
to pattern matching, a tool for analyzing finite data, we develop the
concept of copattern matching, which allows us to synthesize infinite
data. This leads to a symmetric language design where pattern matching
on finite and infinite data can be mixed. We present a core language
for programming with infinite structures by observations together with
its operational semantics based on (co)pattern matching and describe
coverage of copatterns. Our language naturally supports both
call-by-name and call-by-value interpretations and can be seamlessly
integrated into existing languages like Haskell and ML. We prove type
soundness for our language and sketch how copatterns open new
directions for solving problems in the interaction of coinductive and
Codata has been often discussed here and elsewhere. See notably the
discussion on Turner's Total Functional
Programming (historical note: this 2004 beautification of the
original 1995 paper which had much of the same ideas), and on the
language. Given those precedents, it would be easy for the quick
reader to "meh" on the novelty of putting "observation" first
(elimination rather than introduction rules) when talking about
codata; yet the above paper is the first concrete, usable presentation
of an observation in a practical setting that feels right,
and it solves long-standing problem that current dependently-typed
languages (Coq and Agda) have.
Coinduction has an even more prominent role, due to its massive use
to define program equivalence in concurrent process calculi; the
relevant LtU discussion being about Davide Sangiorgi's On the origins of
Bisimulation, Coinduction, and Fixed Points. The POPL'13 paper
doesn't really tell us how coinduction should be seen with
copatterns. It does not adress the question of termination, which is
the topic of the more recent ICFP'13 paper, but I would say that the
answer on that point feels less definitive.
The Size-Change Termination Principle for Constructor Based Languages, by Pierre Hyvernat:
This paper describes an automatic termination checker for a generic first-order call-by-value language in ML style. We use the fact that value are built from variants and tuples to keep some information about how arguments of recursive call evolve during evaluation. The result is a criterion for termination extending the size-change termination principle of Lee, Jones and Ben-Amram that can detect size changes inside subvalues of arguments. Moreover the corresponding algorithm is easy to implement, making it a good candidate for experimentation.
Looks like a relatively straightforward and complete description of a termination checker based on a notion of 'sized types' limited to first-order programs. LtU has covered this topic before, although this new paper doesn't seem to reference that particular Abel work.
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 ï¬rst-class 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 first-class 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 almost-but-not-quite generalizations of existing concepts, like "onions" which are kind of a type-indexed 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 First-Class Messages with Match-Functions. 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 "match-functions".
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 first-class 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 index-passing 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 8-lecture 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 depedently-typed 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 double-life containers lead as â€œinteraction structuresâ€ describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductive-recursive 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.