Kent Dybvig (Cadence Research, Cisco Systems) has released the commercial scheme compiler Chez Scheme (scheme.com) as open source on GitHub. Chez Scheme is a native code generating optimizing compiler for R6RS focusing on performance and productivity. It supports cross-compilation, threading, and many other extensions. Current version is 9.4.
I'm excited to see what the community will build with this great tool.
The paper: An Array-Oriented Language with Static Rank Polymorphism
, Justin Slepak, Olin Shivers, and Panagiotis Manolios, Northeastern University, 2014.
The array-computational model pioneered by Iverson’s lan-
guages APL and J offers a simple and expressive solution to the “von
Neumann bottleneck.” It includes a form of rank, or dimensional, poly-
morphism, which renders much of a program’s control structure im-
plicit by lifting base operators to higher-dimensional array structures.
We present the first formal semantics for this model, along with the first
static type system that captures the full power of the core language.
The formal dynamic semantics of our core language, Remora, illu-
minates several of the murkier corners of the model. This allows us to
resolve some of the model’s
elements in more general, regular
ways. Among these, we can generalise the model from SIMD to MIMD
computations, by extending the semantics to permit functions to be lifted
to higher-dimensional arrays in the same way as their arguments.
Our static semantics, a dependent type system of carefully restricted
power, is capable of describing array computations whose dimensions
cannot be determined statically. The type-checking problem is decidable
and the type system is accompanied by the usual soundness theorems.
Our type system’s principal contribution is that it serves to extract the
implicit control structure that provides so much of the language’s expres-
sive power, making this structure explicitly apparent at compile time.
Type Checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance by Eric Allen, Justin Hilburn, Scott Kilpatrick, Victor Luchangco, Sukyoung Ryu, David Chase, Guy L. Steele Jr.:
In previous work, we presented rules for defining overloaded functions that ensure type safety under symmetric multiple dispatch in an object-oriented language with multiple inheritance, and we showed how to check these rules without requiring the entire type hierarchy to be known, thus supporting modularity and extensibility. In this work, we extend these rules to a language that supports parametric polymorphism on both classes and functions.
In a multiple-inheritance language in which any type may be extended by types in other modules, some overloaded functions that might seem valid are correctly rejected by our rules. We explain how these functions can be permitted in a language that additionally supports an exclusion relation among types, allowing programmers to declare “nominal exclusions” and also implicitly imposing exclusion among different instances of each polymorphic type. We give rules for computing the exclusion relation, deriving many type exclusions from declared and implicit ones.
We also show how to check our rules for ensuring the safety of overloaded functions. In particular, we reduce the problem of handling parametric polymorphism to one of determining subtyping relationships among universal and existential types. Our system has been implemented as part of the open-source Fortress compiler.
Fortress was briefly covered here a couple of times, as were multimethods and multiple dispatch, but this paper really generalizes and nicely summarizes previous work on statically typed modular multimethods, and does a good job explaining the typing rules in an accessible way. The integration with parametric polymorphism I think is key to applying multimethods in other domains which may want modular multimethods, but not multiple inheritance.
The Formalization in COQ might also be of interest to some.
Also, another interesting point is Fortress' use of second-class intersection and union types to simplify type checking.
A special-interest group meeting during the ACM CHI 2016 conference in San Jose, CA on the topic of the usability of programming languages. People are invited to attend!
To attend you must be registered for the CHI'2016 conference, and early registration ends March 14:
For more information about the SIG, see:
Programming languages form the interface between programmers (the users) and the computation that they desire the computer to
execute. Although studies exist for some aspects of programming language design (such as conditionals), other aspects have received little or no human factors evaluations. Designers thus have little they can rely on if they want to make new languages highly usable, and users cannot easily chose a language based on usability criteria. This SIG will bring together researchers and practitioners interested in increasing the depth and breadth of studies on the usability of programming languages, and ultimately in improving the usability of future languages.
Jean Yang & Ari Rabkin C is Manly, Python is for “n00bs”: How False Stereotypes Turn Into Technical “Truths”, Model-View-Culture, January 2015.
This is a bit of a change of pace from the usual technically-focused content on LtU, but it seemed like something that might be of interest to LtUers nonetheless. Yang and Rabkin discuss the cultural baggage that comes along with a variety of languages, and the impact it has on how those languages are perceived and used.
"These preconceived biases arise because programming languages are as much social constructs as they are technical ones. A programming language, like a spoken language, is defined not just by syntax and semantics, but also by the people who use it and what they have written. Research shows that the community and libraries, rather than the technical features, are most important in determining the languages people choose. Scientists, for instance, use Python for the good libraries for scientific computing."
There are probably some interesting clues to how and why some languages are adopted while others fall into obscurity (a question that has come up here before). Also, the article includes references to a study conducted by Rabkin and LtU's own Leo Meyerovich.
Temporal Higher Order Contracts
Tim Disney, Cormac Flanagan, Jay McCarthy
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 higher-order 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 non-interference (where contracts cannot influence correct executions) and also a notion of completeness (where contracts can enforce any decidable, prefix-closed 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.
A technical report by Ravi Chugh et al. Abstract:
We present the SKETCH-N-SKETCH editor for Scalable Vector Graphics (SVG) that integrates programmatic and direct manipulation, two modes of interaction with complementary strengths. In SKETCH-N-SKETCH, the user writes a program to generate an output SVG canvas. Then the user may directly manipulate the canvas while the system infers realtime updates to the program in order to match the changes to the output. To achieve this, we propose (i) a technique called trace-based program synthesis that takes program execution history into account in order to constrain the search space and (ii) heuristics for dealing with ambiguities. Based on our experience writing more than 40 examples and from the results of a study with 25 participants, we conclude that SKETCH-N-SKETCH provides a novel and effective work- flow between the boundaries of existing programmatic and direct manipulation systems.
This was demoed at PLDI to a lot of fanfare. Also see some videos. And a demo that you can actually play with, sweet!
Coordinated concurrent programming in Syndicate
Tony Garnock-Jones and Matthias Felleisen.
Most programs interact with the world: via graphical user interfaces, networks, etc. This form of interactivity entails concurrency, and concurrent program components must coordinate their computations. This paper presents Syndicate, a novel design for a coordinated, concurrent programming language. Each concurrent component in Syndicate is a functional actor that participates in scoped conversations. The medium of conversation arranges for message exchanges and coordinates access to common knowledge. As such, Syndicate occupies a novel point in this design space, halfway between actors and threads.
If you want to understand the language, I would recommend looking at sections 1 to 2.2 (motivation and introducory examples) and then jumping at section 5, which presents fairly interesting designs for larger programs.
Concurrent program components must coordinate their computations to realize the overall goals of the program. This coordination takes two forms: the exchange of knowledge and the establishment of frame conditions. In addition, coordination must take into account that reactions to events may call for the creation of new concurrent components or that existing components may disappear due to exceptions or partial failures. In short, coordination poses a major problem to the proper design of effective communicating, concurrent components.
This paper presents Syndicate, a novel language for coordinated concurrent
programming. A Syndicate program consists of functional actors that participate in precisely scoped conversations. So-called networks coordinate these conversations. When needed, they apply a functional actor to an event and its current state; in turn, they receive a new state plus descriptions of actions. These
actions may represent messages for other participants in the conversations or
assertions for a common space of knowledge.
Precise scoping implies a separation of distinct conversations, and hence existence of multiple networks. At the same time, an actor in one network may
have to communicate with an actor in a different network. To accommodate such
situations, Syndicate allows the embedding of one network into another as if
the first were just an actor within the second. In other words, networks simultaneously scope and compose conversations. The resulting tree-structured shape
of networked conversations corresponds both to tree-like arrangements of containers and processes in modern operating systems and to the nesting of layers
in network protocols . Syndicate thus unifies the programming techniques
of distributed programming with those of coordinated concurrent programming.
By construction, Syndicate networks also manage resources. When a new
actor appears in a conversation, a network allocates the necessary resources.
When an actor fails, it deallocates the associated resources. In particular, it
retracts all shared state associated with the actor, thereby making the failure
visible to interested participants. Syndicate thus solves notorious problems of
service discovery and resource management in the coordination of communicating components.
In sum, Syndicate occupies a novel point in the design space of coordinated
concurrent (functional) components (sec. 2), sitting firmly between a thread-
based world with sharing and local-state-only, message-passing actors. Our de-
sign for Syndicate includes two additional contributions: an efficient protocol
for incrementally maintaining the common knowledge base and a trie-based data
structure for efficiently indexing into it (sec. 3). Finally, our paper presents eval-
uations concerning the fundamental performance characteristics of Syndicate
as well as its pragmatics (secs. 4 and 5).
Our examples illustrate the key properties of Syndicate and their unique
combination. Firstly, the box and demand-matcher examples show that Syndicate conversations may involve many parties, generalizing the Actor model’s
point-to-point conversations. At the same time, the file server example shows
that Syndicate conversations are more precisely bounded than those of traditional Actors. Each of its networks crisply delimits its contained conversations,
each of which may therefore use a task-appropriate language of discourse.
Secondly, all three examples demonstrate the shared-dataspace aspect of
Syndicate. Assertions made by one actor can influence other actors, but cannot
directly alter or remove assertions made by others. The box’s content is made
visible through an assertion in the dataspace, and any actor that knows id can
retrieve the assertion. The demand-matcher responds to changes in the dataspace that denote the existence of new conversations. The file server makes file
contents available through assertions in the (outer) dataspace, in response to
clients placing subscriptions in that dataspace.
Finally, Syndicate places an upper bound on the lifetimes of entries in the
shared space. Items may be asserted and retracted by actors at will in response
to incoming events, but when an actor crashes, all of its assertions are automatically retracted. If the box actor were to crash during a computation, the
assertion describing its content would be visibly withdrawn, and peers could take
some compensating action. The demand matcher can be enhanced to monitor
supply as well as demand and to take corrective action if some worker instance
exits unexpectedly. The combination of this temporal bound on assertions with
Syndicate’s state change notifications gives good failure-signalling and fault-tolerance properties, improving on those seen in Erlang .
Syndicate draws directly on Network Calculus , which, in turn, has borrowed
elements from Actor models [16,17,18], process calculi [19,20,21,22,23], and actor
languages such as Erlang , Scala , E  and AmbientTalk .
This work makes a new connection to shared-dataspace coordination models , including languages such as Linda  and Concurrent ML (CML) .
Linda’s tuplespaces correspond to Syndicate’s dataspaces, but Linda is “generative,” meaning that its tuples take on independent existence once created.
Syndicate’s assertions instead exist only as long as some actor continues to
assert them, which provides a natural mechanism for managing resources and
dealing with partial failures (sec. 2). Linda research on failure-handling focuses
mostly on atomicity and transactions , though Rowstron introduces agent
wills  and uses them to build a fault-tolerance mechanism. Turning to multiple tuplespaces, the Linda variants Klaim  and Lime  offer multiple
spaces and different forms of mobility. Papadopoulos  surveys the many other
variations; Syndicate’s non-mobile, hierarchical, nameless actors and networks
occupy a hitherto unexplored point in this design space.
Some of the proposed designs were surprising to me. There is a reversal of perspective, from the usual application-centric view of applications being first, with lower-level services hidden under abstraction layers, to a more medium-directed perspective that puts the common communication layer first -- in the example of the TCP/IP stack, this is the OS kernel.
Performance Problems You Can Fix: A Dynamic Analysis of Memoization Opportunities
Luca Della Toffola, Michael Pradel, Thomas Gross
Performance bugs are a prevalent problem and recent research proposes various techniques to identify such bugs. This paper addresses a kind of performance problem that often is easy to address but difficult to identify: redundant computations that may be avoided by reusing already computed results for particular inputs, a technique called memoization. To help developers find and use memoization opportunities, we present MemoizeIt, a dynamic analysis that identifies methods that repeatedly perform the same computation. The key idea is to compare inputs and outputs of method calls in a scalable yet precise way. To avoid the overhead of comparing objects at all method invocations in detail, MemoizeIt first compares objects without following any references and iteratively increases the depth of exploration while shrinking the set of considered methods. After each iteration, the approach ignores methods that cannot benefit from memoization, allowing it to analyze calls to the remaining methods in more detail. For every memoization opportunity that MemoizeIt detects, it provides hints on how to implement memoization, making it easy for the developer to fix the performance issue. Applying MemoizeIt to eleven real-world Java programs reveals nine profitable memoization opportunities, most of which are missed by traditional CPU time profilers, conservative compiler optimizations, and other existing approaches for finding performance bugs. Adding memoization as proposed by MemoizeIt leads to statistically significant speedups by factors between 1.04x and 12.93x.
This paper was recommended by Asumu Takikawa. It is a nice idea, which seems surprisingly effective. The examples they analysed (sadly they don't really explain how they picked the program to study) have a mix of memoization opportunities in fairly different parts of the codebase. There are several examples of what we could call "peripheral communication logic", eg. date formatting stuff, which we could assume is not studied really closely by the programmers focusing more on the problem-domain logic. But there is also an interesting of subtle domain-specific memoization opportunity: an existing cache was over-pessimistic and would reset itself at times where it was in fact not necessary, and this observation corresponds to a non-trivial program invariant.
The authors apparently had some difficulties finding program inputs to exercise profiling. Programs should more often be distributed with "performance-representative inputs", not just functionality-testing inputs. In one example of a linting tool, the provided "standard test" was to feed the code of the linting tool to itself. But this was under a default configuration for which the tools' developers had already fixed all alarms, so the alarm-creating code (which actually had an optimization opportunity) was never exercised by this proposed input.
Note that the caching performed is very lightweight, usually not a full tabulation of the function. Most examples just add a static variable to cache the last (input, output) pair, which is only useful when the same input is typically called several times in a row, but costs very little space.
Among many interesting works,
the POPL 2016
papers have a bunch of nice articles
The Gradualizer: a methodology and algorithm for generating gradual type systems
The Gradualizer: a methodology and algorithm for generating gradual type systems
by Matteo Cimini, Jeremy Siek
Many languages are beginning to integrate dynamic and static
typing. Siek and Taha offered gradual typing as an approach to this
integration that provides the benefits of a coherent and full-span
migration between the two disciplines. However, the literature lacks
a general methodology for designing gradually typed languages. Our
first contribution is to provide such a methodology insofar as the
static aspects of gradual typing are concerned: deriving the gradual
type system and the compilation to the cast calculus.
Based on this methodology, we present the Gradualizer, an algorithm
that generates a gradual type system from a normal type system
(expressed as a logic program) and generates a compiler to the cast
calculus. Our algorithm handles a large class of type systems and
generates systems that are correct with respect to the formal criteria
of gradual typing. We also report on an implementation of the
Gradualizer that takes type systems expressed in lambda-prolog and
outputs their gradually typed version (and compiler to the
cast calculus) in lambda-prolog.
One can think of the Gradualizer as a kind of meta-programming
algorithm that takes a type system in input, and returns a gradual
version of this type system as output. I find it interesting that
these type systems are encoded
programs (a notable use-case for functional
logic programming). This is a very nice way to bridge the gap between
describing a transformation that is "in principle" mechanizable and
An interesting phenomenon happening once you want to implement
these ideas in practice is that it forced the authors to define
precisely many intuitions everyone has when reading the description of
a type system as a system of inference rules. These intuitions are,
broadly, about the relation between the static and the dynamic
semantics of a system, the flow of typing information, and the flow of
values; two occurrences of the same type in a typing rule may play very
different roles, some of which are discussed in this article.
Is Sound Gradual Typing Dead?
Is Sound Gradual Typing Dead?
by Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen
Programmers have come to embrace dynamically typed languages for
prototyping and delivering large and complex systems. When it comes to
maintaining and evolving these systems, the lack of explicit static
typing becomes a bottleneck. In response, researchers have explored
the idea of gradually typed programming languages which allow the
post-hoc addition of type annotations to software written in one of
these “untyped” languages. Some of these new hybrid languages insert
run-time checks at the boundary between typed and untyped code to
establish type soundness for the overall system. With sound gradual
typing programmers can rely on the language implementation to provide
meaningful error messages when “untyped” code misbehaves.
While most research on sound gradual typing has remained theoretical,
the few emerging implementations incur performance overheads due to
these checks. Indeed, none of the publications on this topic come with
a comprehensive performance evaluation; a few report disastrous
numbers on toy benchmarks. In response, this paper proposes
a methodology for evaluating the performance of gradually typed
programming languages. The key is to explore the performance impact of
adding type annotations to different parts of a software system. The
methodology takes takes the idea of a gradual conversion from untyped
to typed seriously and calls for measuring the performance of all
possible conversions of a given untyped benchmark. Finally the paper
validates the proposed methodology using Typed Racket, a mature
implementation of sound gradual typing, and a suite of real-world
programs of various sizes and complexities. Based on the results
obtained in this study, the paper concludes that, given the state of
current implementation technologies, sound gradual typing is
dead. Conversely, it raises the question of how implementations could
reduce the overheads associated with ensuring soundness and how tools
could be used to steer programmers clear from pathological cases.
In a fully dynamic system, typing checks are often superficial
(only the existence of a particular field is tested) and done lazily
(the check is made when the field is accessed). Gradual typing changes
this, as typing assumptions can be made earlier than the value is
used, and range over parts of the program that are not exercised in
all execution branches. This has the potentially counter-intuitive
consequence that the overhead of runtime checks may be sensibly larger
than for fully-dynamic systems. This paper presents a methodology to
evaluate the "annotation space" of a Typed Racket program, studying
how the possible choices of which parts to annotate affect overall
Many would find this article surprisingly grounded in reality for
a POPL paper. It puts the spotlight on a question that is too rarely
discussed, and could be presented as a strong illustration of why it
matters to be serious about implementing our research.
Abstracting Gradual Typing
Abstracting Gradual Typing
by Ronald Garcia, Alison M. Clark, Éric Tanter
Language researchers and designers have extended a wide variety of
type systems to support gradual typing, which enables languages to
seamlessly combine dynamic and static checking. These efforts
consistently demonstrate that designing a satisfactory gradual
counterpart to a static type system is challenging, and this challenge
only increases with the sophistication of the type system. Gradual
type system designers need more formal tools to help them
conceptualize, structure, and evaluate their designs.
In this paper, we propose a new formal foundation for gradual
typing, drawing on principles from abstract interpretation to give
gradual types a semantics in terms of pre-existing static
types. Abstracting Gradual Typing (AGT for short) yields a formal
account of consistency—one of the cornerstones of the gradual typing
approach—that subsumes existing notions of consistency, which were
developed through intuition and ad hoc reasoning.
Given a syntax-directed static typing judgment, the AGT approach
induces a corresponding gradual typing judgment. Then the
subject-reduction proof for the underlying static discipline induces
a dynamic semantics for gradual programs defined over source-language
typing derivations. The AGT approach does not recourse to an
externally justified cast calculus: instead, run-time checks naturally
arise by deducing evidence for consistent judgments during
To illustrate our approach, we develop novel gradually-typed
counterparts for two languages: one with record subtyping and one with
information-flow security types. Gradual languages designed with the
AGT approach satisfy, by construction, the refined criteria for
gradual typing set forth by Siek and colleagues.
At first sight this description seems to overlap with the
Gradualizer work cited above, but in fact the two approaches are
highly complementary. The Abstract Gradual Typing effort seems
mechanizable, but it is far from being implementable in practice as
done in the Gradualizer work. It remains a translation to be done on
paper by skilled expert, although, as standard in abstract
interpretation works, many aspects are deeply computational --
computing the best abstractions. On the other hand, it is extremely
powerful to guide system design, as it provides not only a static
semantics for a gradual system, but also a model dynamic
The central idea of the paper is to think of a missing type
annotation not as "a special Dyn type that can contain anything" but
"a specific static type, but I don't know which one it is". A problem
is then to be understood as a family of potential programs, one for
each possible static choice that could have been put there. Not all
choices are consistent (type soundness imposes constraints on
different missing annotations), so we can study the space of possible
interpretations -- using only the original, non-gradually-typed system
to make those deductions.
An obvious consequence is that a static type error occurs exactly
when we can prove that there is no possible consistent typing. A much
less obvious contribution is that, when there is a consistent set of
types, we can consider this set as "evidence" that the program may be
correct, and transport evidence along values while running the
program. This gives a runtime semantics for the gradual system that
automatically does what it should -- but it, of course, would fare
terribly in the performance harness described above.
The Abstract Gradual Typing work feels like a real breakthrough,
and it is interesting to idly wonder about which previous works in
particular enabled this advance. I would make two guesses.
First, there was a very nice conceptualization work in 2015,
drawing general principles from existing gradual typing system, and
highlighting in particular a specific difficulty in designing dynamic
semantics for gradual systems (removing annotations must not make
Refined Criteria for Gradual Typing
by Jeremy Siek, Michael Vitousek, Matteo Cimini, and John Tang Boyland
Siek and Taha  coined the term gradual typing to describe
a theory for integrating static and dynamic typing within a single
language that 1) puts the programmer in control of which regions of
code are statically or dynamically typed and 2) enables the gradual
evolution of code between the two typing disciplines. Since 2006, the
term gradual typing has become quite popular but its meaning has
become diluted to encompass anything related to the integration of
static and dynamic typing. This dilution is partly the fault of the
original paper, which provided an incomplete formal characterization
of what it means to be gradually typed. In this paper we draw a crisp
line in the sand that includes a new formal property, named the
gradual guarantee, that relates the behavior of programs that differ
only with respect to their type annotations. We argue that the gradual
guarantee provides important guidance for designers of gradually typed
languages. We survey the gradual typing literature, critiquing designs
in light of the gradual guarantee. We also report on a mechanized
proof that the gradual guarantee holds for the Gradually Typed Lambda
Second, the marriage of gradual typing and abstract interpretation
was already consumed in previous work (2014), studying the gradual
classification of effects rather than types.
A Theory of Gradual Effect Systems
by Felipe Bañados Schwerter, Ronad Garcia, Éric Tanter
Effect systems have the potential to help software developers, but
their practical adoption has been very limited. We conjecture that
this limited adoption is due in part to the difficulty of
transitioning from a system where effects are implicit and
unrestricted to a system with a static effect discipline, which must
settle for conservative checking in order to be decidable. To address
this hindrance, we develop a theory of gradual effect checking, which
makes it possible to incrementally annotate and statically check
effects, while still rejecting statically inconsistent programs. We
extend the generic type-and-effect framework of Marino and Millstein
with a notion of unknown effects, which turns out to be significantly
more subtle than unknown types in traditional gradual typing. We
appeal to abstract interpretation to develop and validate the concepts
of gradual effect checking. We also demonstrate how an effect system
formulated in Marino and Millstein’s framework can be automatically
extended to support gradual checking.
Difficulty rewards: gradual effects are
more difficult than gradual simply-typed systems, so you get strong
and powerful ideas when you study them. The choice of working on
effect systems is also useful in practice, as nicely said by Philip
Wadler in the conclusion of his 2015
Complement to Blame:
I [Philip Wadler] always assumed gradual types were to help those poor
schmucks using untyped languages to migrate to typed languages. I now
realize that I am one of the poor schmucks. My recent research
involves session types, a linear type system that declares protocols
for sending messages along channels. Sending messages along channels
is an example of an effect. Haskell uses monads to track effects
(Wadler, 1992), and a few experimental languages such as Links
(Cooper et al., 2007), Eff (Bauer and Pretnar, 2014), and Koka
(Leijen, 2014) support effect typing. But, by and large, every
programming language is untyped when it comes to effects. To
encourage migration from legacy code to code with effect types, such
as session types, some form of gradual typing may be essential.